Theorem rexbiia 3209

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2111  ∃wrex 3107

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112

This theorem is referenced by:  rexanid  3215  2rexbiia  3257  ceqsrexbv  3598  reu8  3672  f1oweALT  7655  reldm  7725  seqomlem2  8070  fofinf1o  8783  wdom2d  9028  unbndrank  9255  cfsmolem  9681  fin1a2lem5  9815  fin1a2lem6  9816  infm3  11587  wwlktovfo  14313  even2n  15683  smndex1mnd  18067  cycsubmel  18335  znf1o  20243  lmres  21905  ist1-2  21952  itg2monolem1  24354  lhop1lem  24616  elaa  24912  ulmcau  24990  reeff1o  25042  recosf1o  25127  chpo1ubb  26065  istrkg2ld  26254  wlkswwlksf1o  27665  wwlksnextsurj  27686  nmopnegi  29748  nmop0  29769  nmfn0  29770  adjbd1o  29868  atom1d  30136  abfmpunirn  30415  rearchi  30966  eulerpartgbij  31740  eulerpartlemgh  31746  subfacp1lem3  32542  dfrdg2  33153  heiborlem7  35255  qsresid  35742  eq0rabdioph  39717  elicores  42170  liminfpnfuz  42458  xlimpnfxnegmnf2  42500  fourierdlem70  42818  fourierdlem80  42828  ovolval3  43286  rexrsb  43655