Theorem rexbiia 3112

Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)

Hypothesis

Ref	Expression
rexbiia.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
rexbiia	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem rexbiia

Step	Hyp	Ref	Expression
1		rexbiia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
2	1	pm5.32i 585	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	rexbii2 3110	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3092

This theorem is used by:  rexbii  3114  rexanid  3116  2rexbiia  3228  ceqsrexbv  3617  reu8  3698  f1oweALT  7971  reldm  8043  seqomlem2  8440  fofinf1o  9292  wdom2d  9545  unbndrank  9817  cfsmolem  10265  fin1a2lem5  10399  fin1a2lem6  10400  infm3  12185  wwlktovfo  15014  even2n  16417  smndex1mnd  18995  cycsubmel  19294  znf1o  21730  lmres  23486  ist1-2  23533  itg2monolem1  25938  lhop1lem  26201  elaa  26506  ulmcau  26587  reeff1o  26639  recosf1o  26729  chpo1ubb  27674  noetainflem4  27933  bdayn0sf1o  28592  istrkg2ld  28758  wlkswwlksf1o  30257  wwlksnextsurj  30278  nmopnegi  32346  nmop0  32367  nmfn0  32368  adjbd1o  32466  atom1d  32734  abfmpunirn  33026  rearchi  33689  eulerpartgbij  34786  eulerpartlemgh  34792  noinfepregs  35562  subfacp1lem3  35687  dfrdg2  36298  heiborlem7  38501  qsresid  39013  cxpi11d  43137  fimgmcyc  43335  eq0rabdioph  43540  elicores  46282  liminfpnfuz  46563  xlimpnfxnegmnf2  46605  fourierdlem70  46923  fourierdlem80  46933  ovolval3  47394  rexrsb  47870  slotresfo  49710  basresposfo  49789