Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  opelopabsb Unicode version

Theorem opelopabsb 4220
 Description: The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
Assertion
Ref Expression
opelopabsb
Distinct variable groups:   ,   ,
Allowed substitution hints:   (,)   (,)   ()

Proof of Theorem opelopabsb
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elopab 4218 . . . 4
2 simpl 108 . . . . . . . 8
32eqcomd 2163 . . . . . . 7
4 vex 2715 . . . . . . . 8
5 vex 2715 . . . . . . . 8
64, 5opth 4197 . . . . . . 7
73, 6sylib 121 . . . . . 6
872eximi 1581 . . . . 5
9 eeanv 1912 . . . . . 6
10 isset 2718 . . . . . . 7
11 isset 2718 . . . . . . 7
1210, 11anbi12i 456 . . . . . 6
139, 12bitr4i 186 . . . . 5
148, 13sylib 121 . . . 4
151, 14sylbi 120 . . 3
16 nfv 1508 . . . 4
17 nfv 1508 . . . 4
18 nfs1v 1919 . . . 4
19 nfs1v 1919 . . . . 5
2019nfsbxy 1922 . . . 4
21 sbequ12 1751 . . . . 5
22 sbequ12 1751 . . . . 5
2321, 22sylan9bbr 459 . . . 4
2416, 17, 18, 20, 23cbvopab 4035 . . 3
2515, 24eleq2s 2252 . 2
26 sbcex 2945 . . 3
27 spesbc 3022 . . . 4
28 sbcex 2945 . . . . 5
2928exlimiv 1578 . . . 4
3027, 29syl 14 . . 3
3126, 30jca 304 . 2
32 opeq1 3741 . . . . 5
3332eleq1d 2226 . . . 4
34 dfsbcq2 2940 . . . 4
3533, 34bibi12d 234 . . 3
36 opeq2 3742 . . . . 5
3736eleq1d 2226 . . . 4
38 dfsbcq2 2940 . . . . 5
3938sbcbidv 2995 . . . 4
4037, 39bibi12d 234 . . 3
41 nfopab1 4033 . . . . . 6
4241nfel2 2312 . . . . 5
43 nfs1v 1919 . . . . 5
4442, 43nfbi 1569 . . . 4
45 opeq1 3741 . . . . . 6
4645eleq1d 2226 . . . . 5
47 sbequ12 1751 . . . . 5
4846, 47bibi12d 234 . . . 4
49 nfopab2 4034 . . . . . . 7
5049nfel2 2312 . . . . . 6
51 nfs1v 1919 . . . . . 6
5250, 51nfbi 1569 . . . . 5
53 opeq2 3742 . . . . . . 7
5453eleq1d 2226 . . . . . 6
55 sbequ12 1751 . . . . . 6
5654, 55bibi12d 234 . . . . 5
57 opabid 4217 . . . . 5
5852, 56, 57chvar 1737 . . . 4
5944, 48, 58chvar 1737 . . 3
6035, 40, 59vtocl2g 2776 . 2
6125, 31, 60pm5.21nii 694 1
 Colors of variables: wff set class Syntax hints:   wa 103   wb 104   wceq 1335  wex 1472  wsb 1742   wcel 2128  cvv 2712  wsbc 2937  cop 3563  copab 4024 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169 This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-rex 2441  df-v 2714  df-sbc 2938  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-opab 4026 This theorem is referenced by:  brabsb  4221  opelopabaf  4233  opelopabf  4234  difopab  4718  isarep1  5255
 Copyright terms: Public domain W3C validator