Theorem rexbiia 3077

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  rexbii  3079  rexanid  3081  2rexbiia  3193  ceqsrexbv  3606  reu8  3687  f1oweALT  7904  reldm  7976  seqomlem2  8370  fofinf1o  9216  wdom2d  9466  unbndrank  9735  cfsmolem  10161  fin1a2lem5  10295  fin1a2lem6  10296  infm3  12081  wwlktovfo  14865  even2n  16253  smndex1mnd  18818  cycsubmel  19112  znf1o  21488  lmres  23215  ist1-2  23262  itg2monolem1  25678  lhop1lem  25945  elaa  26251  ulmcau  26331  reeff1o  26384  recosf1o  26471  chpo1ubb  27419  noetainflem4  27679  bdayn0sf1o  28295  0reno  28399  istrkg2ld  28438  wlkswwlksf1o  29857  wwlksnextsurj  29878  nmopnegi  31945  nmop0  31966  nmfn0  31967  adjbd1o  32065  atom1d  32333  abfmpunirn  32634  rearchi  33311  eulerpartgbij  34385  eulerpartlemgh  34391  subfacp1lem3  35226  dfrdg2  35837  heiborlem7  37856  qsresid  38362  cxpi11d  42435  fimgmcyc  42626  eq0rabdioph  42868  elicores  45632  liminfpnfuz  45913  xlimpnfxnegmnf2  45955  fourierdlem70  46273  fourierdlem80  46283  ovolval3  46744  rexrsb  47199  slotresfo  48998  basresposfo  49077