Theorem rexbii2 3021

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

Syntax hints:   ↔ wb 195   ∧ wa 383  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897

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

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-rex 2902

This theorem is referenced by:  rexbiia  3022  rexbii  3023  rexeqbii  3036  rexrab  3337  rexdifsn  4264  reusv2lem4  4798  reusv2  4800  wefrc  5032  wfi  5630  bnd2  8639  rexuz2  11615  rexrp  11729  rexuz3  13936  infpn2  15455  efgrelexlemb  17986  cmpcov2  21003  cmpfi  21021  subislly  21094  txkgen  21265  cubic  24376  sumdmdii  28658  pcmplfin  29255  bnj882  30250  bnj893  30252  frind  30984  heibor1  32779  prtlem100  33161  islmodfg  36657  limcrecl  38696  rexdifpr  40315