This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbccomlemOLD

Description: Obsolete version of sbccomlem as of 20-Aug-2025. (Contributed by NM, 14-Nov-2005) (Revised by Mario Carneiro, 18-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbccomlemOLD ⊢ [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ [˙A / x]˙ φ

Proof

Step Hyp Ref Expression
1 excom ⊢ ∃ x ∃ y x = A ∧ y = B ∧ φ ↔ ∃ y ∃ x x = A ∧ y = B ∧ φ
2 exdistr ⊢ ∃ x ∃ y x = A ∧ y = B ∧ φ ↔ ∃ x x = A ∧ ∃ y y = B ∧ φ
3 an12 ⊢ x = A ∧ y = B ∧ φ ↔ y = B ∧ x = A ∧ φ
4 3 exbii ⊢ ∃ x x = A ∧ y = B ∧ φ ↔ ∃ x y = B ∧ x = A ∧ φ
5 19.42v ⊢ ∃ x y = B ∧ x = A ∧ φ ↔ y = B ∧ ∃ x x = A ∧ φ
6 4 5 bitri ⊢ ∃ x x = A ∧ y = B ∧ φ ↔ y = B ∧ ∃ x x = A ∧ φ
7 6 exbii ⊢ ∃ y ∃ x x = A ∧ y = B ∧ φ ↔ ∃ y y = B ∧ ∃ x x = A ∧ φ
8 1 2 7 3bitr3i ⊢ ∃ x x = A ∧ ∃ y y = B ∧ φ ↔ ∃ y y = B ∧ ∃ x x = A ∧ φ
9 sbc5 ⊢ [˙A / x]˙ ∃ y y = B ∧ φ ↔ ∃ x x = A ∧ ∃ y y = B ∧ φ
10 sbc5 ⊢ [˙B / y]˙ ∃ x x = A ∧ φ ↔ ∃ y y = B ∧ ∃ x x = A ∧ φ
11 8 9 10 3bitr4i ⊢ [˙A / x]˙ ∃ y y = B ∧ φ ↔ [˙B / y]˙ ∃ x x = A ∧ φ
12 sbc5 ⊢ [˙B / y]˙ φ ↔ ∃ y y = B ∧ φ
13 12 sbcbii ⊢ [˙A / x]˙ [˙B / y]˙ φ ↔ [˙A / x]˙ ∃ y y = B ∧ φ
14 sbc5 ⊢ [˙A / x]˙ φ ↔ ∃ x x = A ∧ φ
15 14 sbcbii ⊢ [˙B / y]˙ [˙A / x]˙ φ ↔ [˙B / y]˙ ∃ x x = A ∧ φ
16 11 13 15 3bitr4i ⊢ [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ [˙A / x]˙ φ