Theorem rexbii 1714

Description: Inference adding restricted existential quantifier to both sides of an equivalence.

Hypothesis

Ref	Expression
ralbii.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
rexbii	⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)

Proof of Theorem rexbii

Step	Hyp	Ref	Expression
1		biid 168	. 2 ⊢ (φ ↔ φ)
2	1	hbth 1037	. . 3 ⊢ ((φ ↔ φ) → ∀x(φ ↔ φ))
3		ralbii.1	. . . 4 ⊢ (φ ↔ ψ)
4	3	a1i 8	. . 3 ⊢ ((φ ↔ φ) → (φ ↔ ψ))
5	2, 4	rexbid 1708	. 2 ⊢ ((φ ↔ φ) → (∃x ∈ A φ ↔ ∃x ∈ A ψ))
6	1, 5	ax-mp 7	1 ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)

Syntax hints:   ↔ wb 144  ∃wrex 1692

This theorem is referenced by:  2rexbii 1716  rexanali 1730  r19.29r 1803  r19.42v 1810  reeanv 1824  rexcom4 1870  ceqsrex2v 1936  reu7 1981  0el 2349  uni0b 2590  iuncom 2639  iuniin 2641  iunrab 2664  iinss 2668  iunn0 2676  iunin2 2677  iundif2 2679  iunun 2683  iununi 2686  iunpwss 2691  dffr2 2949  dfepfr 2960  epfrc 2961  sucel 3046  reuxfr 3127  iunpw 3137  iunxpf 3305  cnvuni 3392  dffr3 3523  dminxp 3568  imaco 3604  coiun 3608  isarep1 3683  iunfopab 3719  abrexexlem2 3973  imaiun 3978  abrexex2 3985  elrnoprabg 4186  dfrdg2 4234  rdglem1 4238  tz7.49 4260  uniqs 4436  qsid 4442  zfregcl 4738  zfreg 4739  zfreg2 4740  ac6n 4903  kmlem7 4917  kmlem13 4923  numth2 4931  zorn2lem7 4940  zorn 4943  brdom7disj 4950  brdom6disj 4951  isinfcard 5037  ssxr 5694  dfinfmr 6235  infmsup 6236  supxrre 6251  infmxrcl 6254  uzwo 6582  uzwoOLD 6583  nnwof 6586  cau3iri 7118  cbvsumi 7189  clmnnsi 7287  climunii 7301  climresi 7308  infcvglem1 7425  ivthlem6 7491  efaddlem27 7569  tgval2 7829  blrn2 8052  lmbrnns 8153  lmcvgnns 8154  bcthlem33 8242  isgrp2i 8293  axgroth4 9052  grothpw 9054  axgroth5 9055  grothprim 9057  axhcompl 9143  hhcmpl 9345  hlimuniii 9384  shne0i 9647  nmcopexlem1 10230  nmcopexlem2 10231  nmcfnexlem1 10259  nmcfnexlem2 10260  cdj3lem3b 10649  negcmpprcal2 10724  ntunte 10728  sallnei 11016  subsp 11056  lpni 11417  fictblem 11422  fictb 11423  ordtypelem4 11430  compcov 11486  hscptsscld 11491  reconnlem1 11507  is1stc3 11530  locfincomp 11575  neibastop2lem3 11582  neibastop2lem4 11583  ist0-2 11600  isufil2 11650  ufileu 11658  limfilcf 11683  hausfillim 11685  fcluscf 11724  flimfnfcls 11727  filnetlem2 11764  abrexex2g 11825  sdc 11877  txbas 11973  isbnd3 11997  heiborlem8 12018  heiborlem29 12039  ismrer1 12080

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-rex 1696

Copyright terms: Public domain