Theorem rexbii2 3106

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813  df-rex 3088

This theorem is used by:  rexbiia  3108  rexeqbii  3334  rexrab  3654  rexin  4196  rexdifpr  4620  rexdifsn  4757  reusv2lem4  5363  reusv2  5365  frpoind  6344  eldifsucnn  8666  frind  9747  rexuz2  13019  rexrp  13136  rexuz3  15509  infpn2  17084  efgrelexlemb  19957  cmpcov2  23701  cmpfi  23719  txkgen  23964  cubic  27170  madeval2  28212  sumdmdii  33010  extdgfialglem1  34317  bnj882  35549  bnj893  35551  heibor1  38724  eldmqsres  39205  prtlem100  39896  islmodfg  44055  iuneq1i  46070  limcrecl  46610