Theorem rexbiia 3108

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

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

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 3088

This theorem is used by:  rexbii  3110  rexanid  3112  2rexbiia  3224  ceqsrexbv  3610  reu8  3691  f1oweALT  7982  reldm  8053  seqomlem2  8454  fofinf1o  9314  wdom2d  9567  unbndrank  9848  cfsmolem  10341  fin1a2lem5  10475  fin1a2lem6  10476  infm3  12269  wwlktovfo  15104  even2n  16505  smndex1mnd  19102  cycsubmel  19408  znf1o  21850  lmres  23611  ist1-2  23658  itg2monolem1  26064  lhop1lem  26326  elaa  26632  ulmcau  26715  reeff1o  26767  recosf1o  26856  chpo1ubb  27801  noetainflem4  28090  bdayn0sf1o  28749  istrkg2ld  28915  wlkswwlksf1o  30461  wwlksnextsurj  30482  nmopnegi  32560  nmop0  32581  nmfn0  32582  adjbd1o  32680  atom1d  32948  abfmpunirn  33239  rearchi  33900  eulerpartgbij  34997  eulerpartlemgh  35003  noinfepregs  35784  subfacp1lem3  35926  dfrdg2  36537  heiborlem7  38731  qsresid  39243  cxpi11d  43374  fimgmcyc  43578  eq0rabdioph  43766  elicores  46514  liminfpnfuz  46795  xlimpnfxnegmnf2  46837  fourierdlem70  47155  fourierdlem80  47165  ovolval3  47626  rexrsb  48139  slotresfo  49976  basresposfo  50055