Theorem rexbii2 3211

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

Syntax hints:   ↔ wb 207   ∧ wa 396  ∃wex 1765   ∈ wcel 2083  ∃wrex 3108

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

This theorem depends on definitions:  df-bi 208  df-ex 1766  df-rex 3113

This theorem is referenced by:  rexbiia  3212  rexbii  3213  rexeqbii  3289  rexrab  3628  rexin  4142  rexdifpr  4509  rexdifsn  4640  reusv2lem4  5200  reusv2  5202  wfi  6063  rexuz2  12152  rexrp  12264  rexuz3  14546  infpn2  16082  efgrelexlemb  18607  cmpcov2  21686  cmpfi  21704  txkgen  21948  cubic  25112  sumdmdii  29879  bnj882  31810  bnj893  31812  frpoind  32691  frind  32696  madeval2  32901  heibor1  34641  eldmqsres  35096  prtlem100  35547  islmodfg  39175  limcrecl  41473