Theorem rexbiia 3075

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 574	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	rexbii2 3073	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  rexbii  3077  rexanid  3079  2rexbiia  3199  ceqsrexbv  3625  reu8  3707  f1oweALT  7954  reldm  8026  seqomlem2  8422  fofinf1o  9290  wdom2d  9540  unbndrank  9802  cfsmolem  10230  fin1a2lem5  10364  fin1a2lem6  10365  infm3  12149  wwlktovfo  14931  even2n  16319  smndex1mnd  18844  cycsubmel  19139  znf1o  21468  lmres  23194  ist1-2  23241  itg2monolem1  25658  lhop1lem  25925  elaa  26231  ulmcau  26311  reeff1o  26364  recosf1o  26451  chpo1ubb  27399  noetainflem4  27659  bdayn0sf1o  28266  0reno  28355  istrkg2ld  28394  wlkswwlksf1o  29816  wwlksnextsurj  29837  nmopnegi  31901  nmop0  31922  nmfn0  31923  adjbd1o  32021  atom1d  32289  abfmpunirn  32583  rearchi  33324  eulerpartgbij  34370  eulerpartlemgh  34376  subfacp1lem3  35176  dfrdg2  35790  heiborlem7  37818  qsresid  38320  cxpi11d  42338  fimgmcyc  42529  eq0rabdioph  42771  elicores  45538  liminfpnfuz  45821  xlimpnfxnegmnf2  45863  fourierdlem70  46181  fourierdlem80  46191  ovolval3  46652  rexrsb  47105  slotresfo  48891  basresposfo  48970