Theorem rexbii2 3039

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

Syntax hints:   ↔ wb 196   ∧ wa 384  ∃wex 1704   ∈ wcel 1990  ∃wrex 2913

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

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-rex 2918

This theorem is referenced by:  rexbiia  3040  rexbii  3041  rexeqbii  3054  rexrab  3370  rexdifpr  4205  rexdifsn  4323  reusv2lem4  4872  reusv2  4874  wefrc  5108  wfi  5713  bnd2  8756  rexuz2  11739  rexrp  11853  rexuz3  14088  infpn2  15617  efgrelexlemb  18163  cmpcov2  21193  cmpfi  21211  subislly  21284  txkgen  21455  cubic  24576  sumdmdii  29274  pcmplfin  29927  bnj882  30996  bnj893  30998  imaindm  31682  frind  31740  madeval2  31936  heibor1  33609  eldmqsres  34051  prtlem100  34144  islmodfg  37639  limcrecl  39861