Theorem rexbii2 3032

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

Syntax hints:   ↔ wb 196   ∧ wa 384  ∃wex 1701   ∈ wcel 1987  ∃wrex 2908

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

This theorem depends on definitions:  df-bi 197  df-ex 1702  df-rex 2913

This theorem is referenced by:  rexbiia  3033  rexbii  3034  rexeqbii  3047  rexrab  3352  rexdifpr  4176  rexdifsn  4292  reusv2lem4  4832  reusv2  4834  wefrc  5068  wfi  5672  bnd2  8700  rexuz2  11683  rexrp  11797  rexuz3  14022  infpn2  15541  efgrelexlemb  18084  cmpcov2  21103  cmpfi  21121  subislly  21194  txkgen  21365  cubic  24476  sumdmdii  29123  pcmplfin  29709  bnj882  30704  bnj893  30706  frind  31441  heibor1  33241  prtlem100  33623  islmodfg  37119  limcrecl  39265