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

Theorem ax11el 1813
Description: Basis step for constructing a substitution instance of ax-11o 1491 without using ax-11o 1491. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.)
Assertion
Ref Expression
ax11el

Proof of Theorem ax11el
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 19.26 1240 . . 3
2 elequ1 1402 . . . . . . . . 9
3 elequ2 1403 . . . . . . . . 9
42, 3bitrd 175 . . . . . . . 8
54adantl 260 . . . . . . 7
6 ax-17 1280 . . . . . . . . . 10
7 ax-17 1280 . . . . . . . . . 10
8 elequ1 1402 . . . . . . . . . . 11
9 elequ2 1403 . . . . . . . . . . 11
108, 9bitrd 175 . . . . . . . . . 10
116, 7, 10dvelimfALT 1417 . . . . . . . . 9
124biimprcd 147 . . . . . . . . . 10
1312alimi 1224 . . . . . . . . 9
1411, 13syl6 27 . . . . . . . 8
1514adantr 259 . . . . . . 7
165, 15sylbid 137 . . . . . 6
1716adantl 260 . . . . 5
18 elequ1 1402 . . . . . . . . 9
19 elequ2 1403 . . . . . . . . 9
2018, 19sylan9bb 432 . . . . . . . 8
2120a4s 1296 . . . . . . 7
22 hba1 1299 . . . . . . . 8
2321imbi2d 217 . . . . . . . 8
2422, 23albid 1239 . . . . . . 7
2521, 24imbi12d 221 . . . . . 6
2625adantr 259 . . . . 5
2717, 26mpbid 133 . . . 4
2827exp32 344 . . 3
291, 28sylbir 123 . 2
30 elequ1 1402 . . . . . . 7
3130ad2antll 458 . . . . . 6
32 ax-15 1662 . . . . . . . . 9
3332impcom 114 . . . . . . . 8
3433adantrr 445 . . . . . . 7
3530biimprcd 147 . . . . . . . 8
3635alimi 1224 . . . . . . 7
3734, 36syl6 27 . . . . . 6
3831, 37sylbid 137 . . . . 5
3938adantll 442 . . . 4
40 elequ1 1402 . . . . . . 7
4140a4s 1296 . . . . . 6
4241imbi2d 217 . . . . . . 7
4342dral2 1419 . . . . . 6
4441, 43imbi12d 221 . . . . 5
4544ad2antrr 454 . . . 4
4639, 45mpbid 133 . . 3
4746exp32 344 . 2
48 elequ2 1403 . . . . . . 7
4948ad2antll 458 . . . . . 6
50 ax-15 1662 . . . . . . . . 9
5150imp 113 . . . . . . . 8
5251adantrr 445 . . . . . . 7
5348biimprcd 147 . . . . . . . 8
5453alimi 1224 . . . . . . 7
5552, 54syl6 27 . . . . . 6
5649, 55sylbid 137 . . . . 5
5756adantlr 443 . . . 4
5819a4s 1296 . . . . . 6
5958imbi2d 217 . . . . . . 7
6059dral2 1419 . . . . . 6
6158, 60imbi12d 221 . . . . 5
6261ad2antlr 456 . . . 4
6357, 62mpbid 133 . . 3
6463exp32 344 . 2
65 a9e 1389 . . . . 5
66 a9e 1389 . . . . . . 7
67 ax-1 5 . . . . . . . . . . 11
6867alrimiv 1558 . . . . . . . . . 10
69 elequ1 1402 . . . . . . . . . . . . 13
70 elequ2 1403 . . . . . . . . . . . . 13
7169, 70sylan9bb 432 . . . . . . . . . . . 12
7271adantl 260 . . . . . . . . . . 11
73 dveeq2 1483 . . . . . . . . . . . . . . 15
74 dveeq2 1483 . . . . . . . . . . . . . . 15
7573, 74im2anan9 511 . . . . . . . . . . . . . 14
7675imp 113 . . . . . . . . . . . . 13
77 19.26 1240 . . . . . . . . . . . . 13
7876, 77sylibr 135 . . . . . . . . . . . 12
79 hba1 1299 . . . . . . . . . . . . 13
8071a4s 1296 . . . . . . . . . . . . . 14
8180imbi2d 217 . . . . . . . . . . . . 13
8279, 81albid 1239 . . . . . . . . . . . 12
8378, 82syl 13 . . . . . . . . . . 11
8472, 83imbi12d 221 . . . . . . . . . 10
8568, 84mpbii 134 . . . . . . . . 9
8685exp32 344 . . . . . . . 8
8786exlimdv 1487 . . . . . . 7
8866, 87mpi 14 . . . . . 6
8988exlimdv 1487 . . . . 5
9065, 89mpi 14 . . . 4
9190a1d 20 . . 3
9291a1d 20 . 2
9329, 47, 64, 924cases 1786 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 95   wb 96  wal 1214  wex 1253
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-in1 526  ax-in2 527  ax-io 606  ax-3 714  ax-5 1215  ax-6 1216  ax-7 1217  ax-gen 1218  ax-ie1 1254  ax-ie2 1255  ax-8 1266  ax-10 1267  ax-11 1268  ax-i12 1270  ax-4 1271  ax-13 1274  ax-14 1275  ax-17 1280  ax-i9 1282  ax-ial 1293  ax-i5r 1294  ax-15 1662
This theorem depends on definitions:  df-bi 108
  Copyright terms: Public domain W3C validator