Theorem rexbii2 3089

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

Syntax hints:   ↔ wb 205   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∃wrex 3069

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

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-rex 3070

This theorem is referenced by:  rexbiia  3091  rexeqbii  3314  rexrab  3657  rexin  4204  rexdifpr  4624  rexdifsn  4759  reusv2lem4  5361  reusv2  5363  frpoind  6301  wfiOLD  6310  eldifsucnn  8615  frind  9695  rexuz2  12833  rexrp  12945  rexuz3  15245  infpn2  16796  efgrelexlemb  19546  cmpcov2  22778  cmpfi  22796  txkgen  23040  cubic  26236  madeval2  27226  sumdmdii  31420  bnj882  33627  bnj893  33629  heibor1  36342  eldmqsres  36820  prtlem100  37394  islmodfg  41454  limcrecl  43990