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 ]. ph <-> [. B / y ]. [. A / x ]. ph )

Proof

Step Hyp Ref Expression
1 sbcex 
 |-  ( [. A / x ]. [. B / y ]. ph -> A e. _V )
2 sbcex 
 |-  ( [. B / y ]. [. A / x ]. ph -> B e. _V )
3 sbc6g 
 |-  ( B e. _V -> ( [. B / y ]. [. A / x ]. ph <-> A. y ( y = B -> [. A / x ]. ph ) ) )
4 isset 
 |-  ( B e. _V <-> E. y y = B )
5 exim 
 |-  ( A. y ( y = B -> [. A / x ]. ph ) -> ( E. y y = B -> E. y [. A / x ]. ph ) )
6 4 5 biimtrid 
 |-  ( A. y ( y = B -> [. A / x ]. ph ) -> ( B e. _V -> E. y [. A / x ]. ph ) )
7 sbcex 
 |-  ( [. A / x ]. ph -> A e. _V )
8 7 exlimiv 
 |-  ( E. y [. A / x ]. ph -> A e. _V )
9 6 8 syl6com 
 |-  ( B e. _V -> ( A. y ( y = B -> [. A / x ]. ph ) -> A e. _V ) )
10 3 9 sylbid 
 |-  ( B e. _V -> ( [. B / y ]. [. A / x ]. ph -> A e. _V ) )
11 2 10 mpcom 
 |-  ( [. B / y ]. [. A / x ]. ph -> A e. _V )
12 1 11 pm5.21ni 
 |-  ( -. A e. _V -> ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. [. A / x ]. ph ) )
13 sbc6g 
 |-  ( A e. _V -> ( [. A / x ]. [. B / y ]. ph <-> A. x ( x = A -> [. B / y ]. ph ) ) )
14 isset 
 |-  ( A e. _V <-> E. x x = A )
15 exim 
 |-  ( A. x ( x = A -> [. B / y ]. ph ) -> ( E. x x = A -> E. x [. B / y ]. ph ) )
16 14 15 biimtrid 
 |-  ( A. x ( x = A -> [. B / y ]. ph ) -> ( A e. _V -> E. x [. B / y ]. ph ) )
17 sbcex 
 |-  ( [. B / y ]. ph -> B e. _V )
18 17 exlimiv 
 |-  ( E. x [. B / y ]. ph -> B e. _V )
19 16 18 syl6com 
 |-  ( A e. _V -> ( A. x ( x = A -> [. B / y ]. ph ) -> B e. _V ) )
20 13 19 sylbid 
 |-  ( A e. _V -> ( [. A / x ]. [. B / y ]. ph -> B e. _V ) )
21 1 20 mpcom 
 |-  ( [. A / x ]. [. B / y ]. ph -> B e. _V )
22 21 2 pm5.21ni 
 |-  ( -. B e. _V -> ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. [. A / x ]. ph ) )
23 bi2.04 
 |-  ( ( x = A -> ( y = B -> ph ) ) <-> ( y = B -> ( x = A -> ph ) ) )
24 23 2albii 
 |-  ( A. x A. y ( x = A -> ( y = B -> ph ) ) <-> A. x A. y ( y = B -> ( x = A -> ph ) ) )
25 alcom 
 |-  ( A. x A. y ( y = B -> ( x = A -> ph ) ) <-> A. y A. x ( y = B -> ( x = A -> ph ) ) )
26 24 25 bitri 
 |-  ( A. x A. y ( x = A -> ( y = B -> ph ) ) <-> A. y A. x ( y = B -> ( x = A -> ph ) ) )
27 19.21v 
 |-  ( A. y ( x = A -> ( y = B -> ph ) ) <-> ( x = A -> A. y ( y = B -> ph ) ) )
28 27 albii 
 |-  ( A. x A. y ( x = A -> ( y = B -> ph ) ) <-> A. x ( x = A -> A. y ( y = B -> ph ) ) )
29 19.21v 
 |-  ( A. x ( y = B -> ( x = A -> ph ) ) <-> ( y = B -> A. x ( x = A -> ph ) ) )
30 29 albii 
 |-  ( A. y A. x ( y = B -> ( x = A -> ph ) ) <-> A. y ( y = B -> A. x ( x = A -> ph ) ) )
31 26 28 30 3bitr3i 
 |-  ( A. x ( x = A -> A. y ( y = B -> ph ) ) <-> A. y ( y = B -> A. x ( x = A -> ph ) ) )
32 31 a1i 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A. x ( x = A -> A. y ( y = B -> ph ) ) <-> A. y ( y = B -> A. x ( x = A -> ph ) ) ) )
33 sbc6g 
 |-  ( B e. _V -> ( [. B / y ]. ph <-> A. y ( y = B -> ph ) ) )
34 33 imbi2d 
 |-  ( B e. _V -> ( ( x = A -> [. B / y ]. ph ) <-> ( x = A -> A. y ( y = B -> ph ) ) ) )
35 34 albidv 
 |-  ( B e. _V -> ( A. x ( x = A -> [. B / y ]. ph ) <-> A. x ( x = A -> A. y ( y = B -> ph ) ) ) )
36 35 adantl 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A. x ( x = A -> [. B / y ]. ph ) <-> A. x ( x = A -> A. y ( y = B -> ph ) ) ) )
37 sbc6g 
 |-  ( A e. _V -> ( [. A / x ]. ph <-> A. x ( x = A -> ph ) ) )
38 37 imbi2d 
 |-  ( A e. _V -> ( ( y = B -> [. A / x ]. ph ) <-> ( y = B -> A. x ( x = A -> ph ) ) ) )
39 38 albidv 
 |-  ( A e. _V -> ( A. y ( y = B -> [. A / x ]. ph ) <-> A. y ( y = B -> A. x ( x = A -> ph ) ) ) )
40 39 adantr 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A. y ( y = B -> [. A / x ]. ph ) <-> A. y ( y = B -> A. x ( x = A -> ph ) ) ) )
41 32 36 40 3bitr4d 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A. x ( x = A -> [. B / y ]. ph ) <-> A. y ( y = B -> [. A / x ]. ph ) ) )
42 13 adantr 
 |-  ( ( A e. _V /\ B e. _V ) -> ( [. A / x ]. [. B / y ]. ph <-> A. x ( x = A -> [. B / y ]. ph ) ) )
43 3 adantl 
 |-  ( ( A e. _V /\ B e. _V ) -> ( [. B / y ]. [. A / x ]. ph <-> A. y ( y = B -> [. A / x ]. ph ) ) )
44 41 42 43 3bitr4d 
 |-  ( ( A e. _V /\ B e. _V ) -> ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. [. A / x ]. ph ) )
45 12 22 44 ecase 
 |-  ( [. A / x ]. [. B / y ]. ph <-> [. B / y ]. [. A / x ]. ph )