Theorem rexbiia 3246

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 577	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓))
3	2	rexbii2 3245	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2110  ∃wrex 3139

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-rex 3144

This theorem is referenced by:  rexanid  3252  2rexbiia  3298  ceqsrexbv  3650  reu8  3724  f1oweALT  7667  reldm  7737  seqomlem2  8081  fofinf1o  8793  wdom2d  9038  unbndrank  9265  cfsmolem  9686  fin1a2lem5  9820  fin1a2lem6  9821  infm3  11594  wwlktovfo  14316  even2n  15685  smndex1mnd  18069  cycsubmel  18337  znf1o  20692  lmres  21902  ist1-2  21949  itg2monolem1  24345  lhop1lem  24604  elaa  24899  ulmcau  24977  reeff1o  25029  recosf1o  25113  chpo1ubb  26051  istrkg2ld  26240  wlkswwlksf1o  27651  wwlksnextsurj  27672  nmopnegi  29736  nmop0  29757  nmfn0  29758  adjbd1o  29856  atom1d  30124  abfmpunirn  30391  rearchi  30910  eulerpartgbij  31625  eulerpartlemgh  31631  subfacp1lem3  32424  dfrdg2  33035  heiborlem7  35089  qsresid  35576  eq0rabdioph  39366  elicores  41801  liminfpnfuz  42089  xlimpnfxnegmnf2  42131  fourierdlem70  42454  fourierdlem80  42464  ovolval3  42922  rexrsb  43291