Theorem rexbiia 3180

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  ∃wrex 3065

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3070

This theorem is referenced by:  rexbii  3181  rexanid  3183  2rexbiia  3227  ceqsrexbv  3586  reu8  3668  f1oweALT  7815  reldm  7885  seqomlem2  8282  fofinf1o  9094  wdom2d  9339  unbndrank  9600  cfsmolem  10026  fin1a2lem5  10160  fin1a2lem6  10161  infm3  11934  wwlktovfo  14673  even2n  16051  smndex1mnd  18549  cycsubmel  18819  znf1o  20759  lmres  22451  ist1-2  22498  itg2monolem1  24915  lhop1lem  25177  elaa  25476  ulmcau  25554  reeff1o  25606  recosf1o  25691  chpo1ubb  26629  istrkg2ld  26821  wlkswwlksf1o  28244  wwlksnextsurj  28265  nmopnegi  30327  nmop0  30348  nmfn0  30349  adjbd1o  30447  atom1d  30715  abfmpunirn  30989  rearchi  31546  eulerpartgbij  32339  eulerpartlemgh  32345  subfacp1lem3  33144  dfrdg2  33771  noetainflem4  33943  heiborlem7  35975  qsresid  36460  eq0rabdioph  40598  elicores  43071  liminfpnfuz  43357  xlimpnfxnegmnf2  43399  fourierdlem70  43717  fourierdlem80  43727  ovolval3  44185  rexrsb  44592