Theorem rexbii2 3104

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

Syntax hints:   ↔ wb 208   ∧ wa 399  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-ex 1799  df-rex 3086

This theorem is referenced by:  rexbiia  3106  rexeqbii  3334  rexrab  3658  rexin  4202  rexdifpr  4617  rexdifsn  4753  reusv2lem4  5357  reusv2  5359  frpoind  6325  eldifsucnn  8629  frind  9705  rexuz2  12897  rexrp  13013  rexuz3  15359  infpn2  16932  efgrelexlemb  19773  cmpcov2  23430  cmpfi  23448  txkgen  23692  cubic  26891  madeval2  27903  sumdmdii  32564  extdgfialglem1  33950  bnj882  35185  bnj893  35187  heibor1  38273  eldmqsres  38756  prtlem100  39447  islmodfg  43610  iuneq1i  45628  limcrecl  46169