Theorem rexbiia 3111

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

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

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 3091

This theorem is used by:  rexbii  3113  rexanid  3115  2rexbiia  3227  ceqsrexbv  3613  reu8  3694  f1oweALT  8018  reldmOLD  8090  seqomlem2  8499  fofinf1o  9359  wdom2d  9611  unbndrank  9892  cfsmolem  10387  fin1a2lem5  10521  fin1a2lem6  10522  infm3  12316  wwlktovfo  15154  even2n  16556  smndex1mnd  19159  cycsubmel  19465  znf1o  21912  lmres  23673  ist1-2  23720  itg2monolem1  26126  lhop1lem  26388  elaa  26696  ulmcau  26779  reeff1o  26831  recosf1o  26920  chpo1ubb  27865  noetainflem4  28154  bdayn0sf1o  28813  istrkg2ld  28979  wlkswwlksf1o  30525  wwlksnextsurj  30546  nmopnegi  32624  nmop0  32645  nmfn0  32646  adjbd1o  32744  atom1d  33012  abfmpunirn  33344  rearchi  34011  eulerpartgbij  35115  eulerpartlemgh  35121  noinfepregs  35942  subfacp1lem3  36155  dfrdg2  36772  heiborlem7  39017  qsresid  39529  cxpi11d  43660  fimgmcyc  43864  eq0rabdioph  44053  elicores  46818  liminfpnfuz  47099  xlimpnfxnegmnf2  47141  fourierdlem70  47459  fourierdlem80  47469  ovolval3  47930  rexrsb  48444  slotresfo  50344  basresposfo  50423