Theorem rexbiia 3091

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2105  ∃wrex 3069

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 206  df-an 396  df-ex 1781  df-rex 3070

This theorem is referenced by:  rexbii  3093  rexanid  3095  2rexbiia  3214  ceqsrexbv  3644  reu8  3729  f1oweALT  7963  reldm  8034  seqomlem2  8457  fofinf1o  9333  wdom2d  9581  unbndrank  9843  cfsmolem  10271  fin1a2lem5  10405  fin1a2lem6  10406  infm3  12180  wwlktovfo  14916  even2n  16292  smndex1mnd  18833  cycsubmel  19122  znf1o  21417  lmres  23124  ist1-2  23171  itg2monolem1  25600  lhop1lem  25866  elaa  26168  ulmcau  26246  reeff1o  26299  recosf1o  26384  chpo1ubb  27328  noetainflem4  27587  0reno  28106  istrkg2ld  28145  wlkswwlksf1o  29567  wwlksnextsurj  29588  nmopnegi  31652  nmop0  31673  nmfn0  31674  adjbd1o  31772  atom1d  32040  abfmpunirn  32311  rearchi  32898  eulerpartgbij  33836  eulerpartlemgh  33842  subfacp1lem3  34638  dfrdg2  35238  heiborlem7  37151  qsresid  37660  eq0rabdioph  41979  elicores  44707  liminfpnfuz  44993  xlimpnfxnegmnf2  45035  fourierdlem70  45353  fourierdlem80  45363  ovolval3  45824  rexrsb  46269