Metamath Proof Explorer

Theorem sbccomlem

Description: Lemma for sbccom . (Contributed by NM, 14-Nov-2005) (Revised by Mario Carneiro, 18-Oct-2016) Avoid ax-10 , ax-12 . (Revised by SN, 20-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 sbcex ⊢ [˙A / x]˙ [˙B / y]˙ φ → A ∈ V
2 sbcex ⊢ [˙B / y]˙ [˙A / x]˙ φ → B ∈ V
3 sbc6g ⊢ B ∈ V → [˙B / y]˙ [˙A / x]˙ φ ↔ ∀ y y = B → [˙A / x]˙ φ
4 isset ⊢ B ∈ V ↔ ∃ y y = B
5 exim ⊢ ∀ y y = B → [˙A / x]˙ φ → ∃ y y = B → ∃ y [˙A / x]˙ φ
6 4 5 biimtrid ⊢ ∀ y y = B → [˙A / x]˙ φ → B ∈ V → ∃ y [˙A / x]˙ φ
7 sbcex ⊢ [˙A / x]˙ φ → A ∈ V
8 7 exlimiv ⊢ ∃ y [˙A / x]˙ φ → A ∈ V
9 6 8 syl6com ⊢ B ∈ V → ∀ y y = B → [˙A / x]˙ φ → A ∈ V
10 3 9 sylbid ⊢ B ∈ V → [˙B / y]˙ [˙A / x]˙ φ → A ∈ V
11 2 10 mpcom ⊢ [˙B / y]˙ [˙A / x]˙ φ → A ∈ V
12 1 11 pm5.21ni ⊢ ¬ A ∈ V → [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ [˙A / x]˙ φ
13 sbc6g ⊢ A ∈ V → [˙A / x]˙ [˙B / y]˙ φ ↔ ∀ x x = A → [˙B / y]˙ φ
14 isset ⊢ A ∈ V ↔ ∃ x x = A
15 exim ⊢ ∀ x x = A → [˙B / y]˙ φ → ∃ x x = A → ∃ x [˙B / y]˙ φ
16 14 15 biimtrid ⊢ ∀ x x = A → [˙B / y]˙ φ → A ∈ V → ∃ x [˙B / y]˙ φ
17 sbcex ⊢ [˙B / y]˙ φ → B ∈ V
18 17 exlimiv ⊢ ∃ x [˙B / y]˙ φ → B ∈ V
19 16 18 syl6com ⊢ A ∈ V → ∀ x x = A → [˙B / y]˙ φ → B ∈ V
20 13 19 sylbid ⊢ A ∈ V → [˙A / x]˙ [˙B / y]˙ φ → B ∈ V
21 1 20 mpcom ⊢ [˙A / x]˙ [˙B / y]˙ φ → B ∈ V
22 21 2 pm5.21ni ⊢ ¬ B ∈ V → [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ [˙A / x]˙ φ
23 bi2.04 ⊢ x = A → y = B → φ ↔ y = B → x = A → φ
24 23 2albii ⊢ ∀ x ∀ y x = A → y = B → φ ↔ ∀ x ∀ y y = B → x = A → φ
25 alcom ⊢ ∀ x ∀ y y = B → x = A → φ ↔ ∀ y ∀ x y = B → x = A → φ
26 24 25 bitri ⊢ ∀ x ∀ y x = A → y = B → φ ↔ ∀ y ∀ x y = B → x = A → φ
27 19.21v ⊢ ∀ y x = A → y = B → φ ↔ x = A → ∀ y y = B → φ
28 27 albii ⊢ ∀ x ∀ y x = A → y = B → φ ↔ ∀ x x = A → ∀ y y = B → φ
29 19.21v ⊢ ∀ x y = B → x = A → φ ↔ y = B → ∀ x x = A → φ
30 29 albii ⊢ ∀ y ∀ x y = B → x = A → φ ↔ ∀ y y = B → ∀ x x = A → φ
31 26 28 30 3bitr3i ⊢ ∀ x x = A → ∀ y y = B → φ ↔ ∀ y y = B → ∀ x x = A → φ
32 31 a1i ⊢ A ∈ V ∧ B ∈ V → ∀ x x = A → ∀ y y = B → φ ↔ ∀ y y = B → ∀ x x = A → φ
33 sbc6g ⊢ B ∈ V → [˙B / y]˙ φ ↔ ∀ y y = B → φ
34 33 imbi2d ⊢ B ∈ V → x = A → [˙B / y]˙ φ ↔ x = A → ∀ y y = B → φ
35 34 albidv ⊢ B ∈ V → ∀ x x = A → [˙B / y]˙ φ ↔ ∀ x x = A → ∀ y y = B → φ
36 35 adantl ⊢ A ∈ V ∧ B ∈ V → ∀ x x = A → [˙B / y]˙ φ ↔ ∀ x x = A → ∀ y y = B → φ
37 sbc6g ⊢ A ∈ V → [˙A / x]˙ φ ↔ ∀ x x = A → φ
38 37 imbi2d ⊢ A ∈ V → y = B → [˙A / x]˙ φ ↔ y = B → ∀ x x = A → φ
39 38 albidv ⊢ A ∈ V → ∀ y y = B → [˙A / x]˙ φ ↔ ∀ y y = B → ∀ x x = A → φ
40 39 adantr ⊢ A ∈ V ∧ B ∈ V → ∀ y y = B → [˙A / x]˙ φ ↔ ∀ y y = B → ∀ x x = A → φ
41 32 36 40 3bitr4d ⊢ A ∈ V ∧ B ∈ V → ∀ x x = A → [˙B / y]˙ φ ↔ ∀ y y = B → [˙A / x]˙ φ
42 13 adantr ⊢ A ∈ V ∧ B ∈ V → [˙A / x]˙ [˙B / y]˙ φ ↔ ∀ x x = A → [˙B / y]˙ φ
43 3 adantl ⊢ A ∈ V ∧ B ∈ V → [˙B / y]˙ [˙A / x]˙ φ ↔ ∀ y y = B → [˙A / x]˙ φ
44 41 42 43 3bitr4d ⊢ A ∈ V ∧ B ∈ V → [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ [˙A / x]˙ φ
45 12 22 44 ecase ⊢ [˙A / x]˙ [˙B / y]˙ φ ↔ [˙B / y]˙ [˙A / x]˙ φ