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

Theorem ax11el 1811
Description: Basis step for constructing a substitution instance of ax-11o 1654 without using ax-11o 1654. Atomic formula for membership predicate.
Assertion
Ref Expression
ax11el

Proof of Theorem ax11el
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 19.26 1361 . . 3
2 elequ1 1572 . . . . . . . . 9
3 elequ2 1573 . . . . . . . . 9
42, 3bitrd 176 . . . . . . . 8
54adantl 261 . . . . . . 7
6 ax-17 1402 . . . . . . . . . 10
7 ax-17 1402 . . . . . . . . . 10
8 elequ1 1572 . . . . . . . . . . 11
9 elequ2 1573 . . . . . . . . . . 11
108, 9bitrd 176 . . . . . . . . . 10
116, 7, 10dvelimfALT 1585 . . . . . . . . 9
124biimprcd 148 . . . . . . . . . 10
1312alimi 1345 . . . . . . . . 9
1411, 13syl6 28 . . . . . . . 8
1514adantr 260 . . . . . . 7
165, 15sylbid 138 . . . . . 6
1716adantl 261 . . . . 5
18 elequ1 1572 . . . . . . . . 9
19 elequ2 1573 . . . . . . . . 9
2018, 19sylan9bb 434 . . . . . . . 8
2120a4s 1433 . . . . . . 7
22 hba1 1436 . . . . . . . 8
2321imbi2d 218 . . . . . . . 8
2422, 23albid 1360 . . . . . . 7
2521, 24imbi12d 222 . . . . . 6
2625adantr 260 . . . . 5
2717, 26mpbid 134 . . . 4
2827exp32 345 . . 3
291, 28sylbir 124 . 2
30 elequ1 1572 . . . . . . 7
3130ad2antll 459 . . . . . 6
32 ax-15 1807 . . . . . . . . 9
3332impcom 115 . . . . . . . 8
3433adantrr 446 . . . . . . 7
3530biimprcd 148 . . . . . . . 8
3635alimi 1345 . . . . . . 7
3734, 36syl6 28 . . . . . 6
3831, 37sylbid 138 . . . . 5
3938adantll 443 . . . 4
40 elequ1 1572 . . . . . . 7
4140a4s 1433 . . . . . 6
4241imbi2d 218 . . . . . . 7
4342dral2 1587 . . . . . 6
4441, 43imbi12d 222 . . . . 5
4544ad2antrr 455 . . . 4
4639, 45mpbid 134 . . 3
4746exp32 345 . 2
48 elequ2 1573 . . . . . . 7
4948ad2antll 459 . . . . . 6
50 ax-15 1807 . . . . . . . . 9
5150imp 114 . . . . . . . 8
5251adantrr 446 . . . . . . 7
5348biimprcd 148 . . . . . . . 8
5453alimi 1345 . . . . . . 7
5552, 54syl6 28 . . . . . 6
5649, 55sylbid 138 . . . . 5
5756adantlr 444 . . . 4
5819a4s 1433 . . . . . 6
5958imbi2d 218 . . . . . . 7
6059dral2 1587 . . . . . 6
6158, 60imbi12d 222 . . . . 5
6261ad2antlr 457 . . . 4
6357, 62mpbid 134 . . 3
6463exp32 345 . 2
65 a9e 1556 . . . . 5
66 a9e 1556 . . . . . . 7
67 ax-1 5 . . . . . . . . . . 11
6867alrimiv 1723 . . . . . . . . . 10
69 elequ1 1572 . . . . . . . . . . . . 13
70 elequ2 1573 . . . . . . . . . . . . 13
7169, 70sylan9bb 434 . . . . . . . . . . . 12
7271adantl 261 . . . . . . . . . . 11
73 dveeq2 1646 . . . . . . . . . . . . . . 15
74 dveeq2 1646 . . . . . . . . . . . . . . 15
7573, 74im2anan9 512 . . . . . . . . . . . . . 14
7675imp 114 . . . . . . . . . . . . 13
77 19.26 1361 . . . . . . . . . . . . 13
7876, 77sylibr 136 . . . . . . . . . . . 12
79 hba1 1436 . . . . . . . . . . . . 13
8071a4s 1433 . . . . . . . . . . . . . 14
8180imbi2d 218 . . . . . . . . . . . . 13
8279, 81albid 1360 . . . . . . . . . . . 12
8378, 82syl 14 . . . . . . . . . . 11
8472, 83imbi12d 222 . . . . . . . . . 10
8568, 84mpbii 135 . . . . . . . . 9
8685exp32 345 . . . . . . . 8
8786exlimdv 1650 . . . . . . 7
8866, 87mpi 15 . . . . . 6
8988exlimdv 1650 . . . . 5
9065, 89mpi 15 . . . 4
9190a1d 21 . . 3
9291a1d 21 . 2
9329, 47, 64, 924cases 884 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 96   wb 97  wal 1335  wex 1374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-ia1 98  ax-ia2 99  ax-ia3 100  ax-in1 527  ax-in2 528  ax-io 607  ax-5 1336  ax-6 1337  ax-7 1338  ax-gen 1339  ax-ie1 1375  ax-ie2 1376  ax-8 1387  ax-10 1388  ax-11 1389  ax-i12 1391  ax-4 1392  ax-13 1395  ax-14 1396  ax-17 1402  ax-i9 1417  ax-ial 1430  ax-i5r 1431  ax-15 1807
This theorem depends on definitions:  df-bi 109
  Copyright terms: Public domain W3C validator