Theorem rexbiia 3176

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2108  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  rexbii  3177  rexanid  3182  2rexbiia  3226  ceqsrexbv  3579  reu8  3663  f1oweALT  7788  reldm  7858  seqomlem2  8252  fofinf1o  9024  wdom2d  9269  unbndrank  9531  cfsmolem  9957  fin1a2lem5  10091  fin1a2lem6  10092  infm3  11864  wwlktovfo  14601  even2n  15979  smndex1mnd  18464  cycsubmel  18734  znf1o  20671  lmres  22359  ist1-2  22406  itg2monolem1  24820  lhop1lem  25082  elaa  25381  ulmcau  25459  reeff1o  25511  recosf1o  25596  chpo1ubb  26534  istrkg2ld  26725  wlkswwlksf1o  28145  wwlksnextsurj  28166  nmopnegi  30228  nmop0  30249  nmfn0  30250  adjbd1o  30348  atom1d  30616  abfmpunirn  30891  rearchi  31448  eulerpartgbij  32239  eulerpartlemgh  32245  subfacp1lem3  33044  dfrdg2  33677  noetainflem4  33870  heiborlem7  35902  qsresid  36387  eq0rabdioph  40514  elicores  42961  liminfpnfuz  43247  xlimpnfxnegmnf2  43289  fourierdlem70  43607  fourierdlem80  43617  ovolval3  44075  rexrsb  44479