Theorem rexbii2 3083

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 1855	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
3		df-rex 3065	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rex 3065	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜓 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜓))
5	2, 3, 4	3bitr4i 304	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓)

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-rex 3065

This theorem is referenced by:  rexbiia  3085  rexeqbii  3313  rexrab  3644  rexin  4185  rexdifpr  4598  rexdifsn  4734  reusv2lem4  5337  reusv2  5339  frpoind  6300  eldifsucnn  8597  frind  9672  rexuz2  12847  rexrp  12963  rexuz3  15309  infpn2  16882  efgrelexlemb  19723  cmpcov2  23380  cmpfi  23398  txkgen  23642  cubic  26838  madeval2  27850  sumdmdii  32511  extdgfialglem1  33883  bnj882  35115  bnj893  35117  heibor1  38184  eldmqsres  38667  prtlem100  39358  islmodfg  43521  iuneq1i  45539  limcrecl  46081