Theorem rexbii2 3248

Description: Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)

Hypothesis

Ref	Expression
rexbii2.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))

Assertion

Ref	Expression
rexbii2	⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)

Proof of Theorem rexbii2

Step	Hyp	Ref	Expression
1		rexbii2.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜓))
2	1	exbii 1847	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
3		df-rex 3147	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rex 3147	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
5	2, 3, 4	3bitr4i 305	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 208   ∧ wa 398  ∃wex 1779   ∈ wcel 2113  ∃wrex 3142

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 209  df-ex 1780  df-rex 3147

This theorem is referenced by:  rexbiia  3249  rexbii  3250  rexeqbii  3329  rexrab  3690  rexin  4219  rexdifpr  4601  rexdifsn  4730  reusv2lem4  5305  reusv2  5307  wfi  6184  rexuz2  12302  rexrp  12413  rexuz3  14711  infpn2  16252  efgrelexlemb  18879  cmpcov2  22001  cmpfi  22019  txkgen  22263  cubic  25430  sumdmdii  30195  bnj882  32202  bnj893  32204  frpoind  33084  frind  33089  madeval2  33294  heibor1  35092  eldmqsres  35547  prtlem100  35999  islmodfg  39675  limcrecl  41916