Theorem rexbiia 3074

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∃wrex 3053

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rexbii  3076  rexanid  3078  2rexbiia  3198  ceqsrexbv  3622  reu8  3704  f1oweALT  7951  reldm  8023  seqomlem2  8419  fofinf1o  9283  wdom2d  9533  unbndrank  9795  cfsmolem  10223  fin1a2lem5  10357  fin1a2lem6  10358  infm3  12142  wwlktovfo  14924  even2n  16312  smndex1mnd  18837  cycsubmel  19132  znf1o  21461  lmres  23187  ist1-2  23234  itg2monolem1  25651  lhop1lem  25918  elaa  26224  ulmcau  26304  reeff1o  26357  recosf1o  26444  chpo1ubb  27392  noetainflem4  27652  bdayn0sf1o  28259  0reno  28348  istrkg2ld  28387  wlkswwlksf1o  29809  wwlksnextsurj  29830  nmopnegi  31894  nmop0  31915  nmfn0  31916  adjbd1o  32014  atom1d  32282  abfmpunirn  32576  rearchi  33317  eulerpartgbij  34363  eulerpartlemgh  34369  subfacp1lem3  35169  dfrdg2  35783  heiborlem7  37811  qsresid  38313  cxpi11d  42331  fimgmcyc  42522  eq0rabdioph  42764  elicores  45531  liminfpnfuz  45814  xlimpnfxnegmnf2  45856  fourierdlem70  46174  fourierdlem80  46184  ovolval3  46645  rexrsb  47101  slotresfo  48887  basresposfo  48966