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 ( [ 𝐴 / 𝑥 ] [ 𝐵 / 𝑦 ] 𝜑[ 𝐵 / 𝑦 ] [ 𝐴 / 𝑥 ] 𝜑 )

Proof

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