Theorem rexbiia 3081

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 3079	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  rexbii  3083  rexanid  3085  2rexbiia  3197  ceqsrexbv  3610  reu8  3691  f1oweALT  7916  reldm  7988  seqomlem2  8382  fofinf1o  9232  wdom2d  9485  unbndrank  9754  cfsmolem  10180  fin1a2lem5  10314  fin1a2lem6  10315  infm3  12101  wwlktovfo  14881  even2n  16269  smndex1mnd  18835  cycsubmel  19129  znf1o  21506  lmres  23244  ist1-2  23291  itg2monolem1  25707  lhop1lem  25974  elaa  26280  ulmcau  26360  reeff1o  26413  recosf1o  26500  chpo1ubb  27448  noetainflem4  27708  bdayn0sf1o  28366  istrkg2ld  28532  wlkswwlksf1o  29952  wwlksnextsurj  29973  nmopnegi  32040  nmop0  32061  nmfn0  32062  adjbd1o  32160  atom1d  32428  abfmpunirn  32730  rearchi  33427  eulerpartgbij  34529  eulerpartlemgh  34535  noinfepregs  35289  subfacp1lem3  35376  dfrdg2  35987  heiborlem7  38018  qsresid  38524  cxpi11d  42598  fimgmcyc  42789  eq0rabdioph  43018  elicores  45779  liminfpnfuz  46060  xlimpnfxnegmnf2  46102  fourierdlem70  46420  fourierdlem80  46430  ovolval3  46891  rexrsb  47346  slotresfo  49144  basresposfo  49223