rexbii2 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > rexbii2		GIF version

Theorem rexbii2 2643

Description: Inference adding different restricted existential quantifiers to each side of an equivalence. (Contributed by NM, 4-Feb-2004.)

**Hypothesis**
Ref	Expression
rexbii2.1	⊢ ((x ∈ A ∧ φ) ↔ (x ∈ B ∧ ψ))

**Assertion**
Ref	Expression
rexbii2	⊢ (∃x ∈ A φ ↔ ∃x ∈ B ψ)

**Proof of Theorem rexbii2**
Step	Hyp	Ref	Expression
1		rexbii2.1	. . 3 ⊢ ((x ∈ A ∧ φ) ↔ (x ∈ B ∧ ψ))
2	1	exbii 1582	. 2 ⊢ (∃x(x ∈ A ∧ φ) ↔ ∃x(x ∈ B ∧ ψ))
3		df-rex 2620	. 2 ⊢ (∃x ∈ A φ ↔ ∃x(x ∈ A ∧ φ))
4		df-rex 2620	. 2 ⊢ (∃x ∈ B ψ ↔ ∃x(x ∈ B ∧ ψ))
5	2, 3, 4	3bitr4i 268	1 ⊢ (∃x ∈ A φ ↔ ∃x ∈ B ψ)

Colors of variables: wff setvar class

Syntax hints: ↔ wb 176 ∧ wa 358 ∃wex 1541 ∈ wcel 1710 ∃wrex 2615

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557

This theorem depends on definitions: df-bi 177 df-ex 1542 df-rex 2620

This theorem is referenced by: rexeqbii 2645 rexbiia 2647 rexrab 3000 rexdifsn 3843 pw1in 4164