Theorem rexbii2 3177

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

Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1853   ∈ wcel 2139  ∃wrex 3051

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

This theorem depends on definitions:  df-bi 197  df-ex 1854  df-rex 3056

This theorem is referenced by:  rexbiia  3178  rexbii  3179  rexeqbii  3192  rexrab  3511  rexdifpr  4350  rexdifsn  4469  reusv2lem4  5021  reusv2  5023  wefrc  5260  wfi  5874  bnd2  8929  rexuz2  11932  rexrp  12046  rexuz3  14287  infpn2  15819  efgrelexlemb  18363  cmpcov2  21395  cmpfi  21413  subislly  21486  txkgen  21657  cubic  24775  sumdmdii  29583  pcmplfin  30236  bnj882  31303  bnj893  31305  imaindm  31987  frpoind  32046  frind  32049  madeval2  32242  heibor1  33922  eldmqsres  34375  prtlem100  34648  islmodfg  38141  limcrecl  40364