Theorem rexbiia 3174

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

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

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 3076

This theorem is referenced by:  rexbii  3175  rexanid  3180  2rexbiia  3222  ceqsrexbv  3570  reu8  3649  f1oweALT  7683  reldm  7753  seqomlem2  8103  fofinf1o  8845  wdom2d  9090  unbndrank  9317  cfsmolem  9743  fin1a2lem5  9877  fin1a2lem6  9878  infm3  11649  wwlktovfo  14382  even2n  15756  smndex1mnd  18155  cycsubmel  18424  znf1o  20333  lmres  22014  ist1-2  22061  itg2monolem1  24464  lhop1lem  24726  elaa  25025  ulmcau  25103  reeff1o  25155  recosf1o  25240  chpo1ubb  26178  istrkg2ld  26367  wlkswwlksf1o  27778  wwlksnextsurj  27799  nmopnegi  29861  nmop0  29882  nmfn0  29883  adjbd1o  29981  atom1d  30249  abfmpunirn  30526  rearchi  31080  eulerpartgbij  31871  eulerpartlemgh  31877  subfacp1lem3  32673  dfrdg2  33300  noetainflem4  33541  heiborlem7  35570  qsresid  36057  eq0rabdioph  40135  elicores  42581  liminfpnfuz  42869  xlimpnfxnegmnf2  42911  fourierdlem70  43229  fourierdlem80  43239  ovolval3  43697  rexrsb  44082