Theorem rexbiia 3110

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2143  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  rexbii  3112  rexanid  3114  2rexbiia  3226  ceqsrexbv  3616  reu8  3697  f1oweALT  7970  reldm  8042  seqomlem2  8439  fofinf1o  9290  wdom2d  9543  unbndrank  9815  cfsmolem  10255  fin1a2lem5  10389  fin1a2lem6  10390  infm3  12175  wwlktovfo  14997  even2n  16401  smndex1mnd  18973  cycsubmel  19272  znf1o  21682  lmres  23438  ist1-2  23485  itg2monolem1  25890  lhop1lem  26153  elaa  26458  ulmcau  26539  reeff1o  26591  recosf1o  26681  chpo1ubb  27626  noetainflem4  27885  bdayn0sf1o  28544  istrkg2ld  28710  wlkswwlksf1o  30209  wwlksnextsurj  30230  nmopnegi  32298  nmop0  32319  nmfn0  32320  adjbd1o  32418  atom1d  32686  abfmpunirn  32978  rearchi  33647  eulerpartgbij  34743  eulerpartlemgh  34749  noinfepregs  35527  subfacp1lem3  35655  dfrdg2  36266  heiborlem7  38449  qsresid  38961  cxpi11d  43085  fimgmcyc  43285  eq0rabdioph  43490  elicores  46232  liminfpnfuz  46513  xlimpnfxnegmnf2  46555  fourierdlem70  46873  fourierdlem80  46883  ovolval3  47344  rexrsb  47820  slotresfo  49660  basresposfo  49739