Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1379 Structured version   Visualization version   Unicode version

Theorem bnj1379 29714
 Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj1379.1
bnj1379.2
bnj1379.3
bnj1379.5
bnj1379.6
bnj1379.7
Assertion
Ref Expression
bnj1379
Distinct variable groups:   ,,,,,   ,   ,   ,,,
Allowed substitution hints:   (,,,)   (,)   (,,,,)   (,,,,)   (,,,,)   (,,,)

Proof of Theorem bnj1379
StepHypRef Expression
1 bnj1379.3 . . . . 5
2 bnj1379.1 . . . . . . . 8
32bnj1095 29665 . . . . . . 7
43nfi 1682 . . . . . 6
5 nfra1 2785 . . . . . 6
64, 5nfan 2031 . . . . 5
71, 6nfxfr 1704 . . . 4
82bnj946 29658 . . . . . . . 8
98biimpi 199 . . . . . . 7
10919.21bi 1967 . . . . . 6
111, 10bnj832 29640 . . . . 5
12 funrel 5606 . . . . 5
1311, 12syl6 33 . . . 4
147, 13ralrimi 2800 . . 3
15 reluni 4961 . . 3
1614, 15sylibr 217 . 2
17 bnj1379.5 . . . . . 6
18 eluni2 4194 . . . . . . . . . . . 12
1918biimpi 199 . . . . . . . . . . 11
2019bnj1196 29678 . . . . . . . . . 10
2117, 20bnj836 29643 . . . . . . . . 9
22 bnj1379.6 . . . . . . . . 9
23 nfv 1769 . . . . . . . . . . . 12
24 nfv 1769 . . . . . . . . . . . 12
257, 23, 24nf3an 2033 . . . . . . . . . . 11
2617, 25nfxfr 1704 . . . . . . . . . 10
2726nfri 1972 . . . . . . . . 9
2821, 22, 27bnj1345 29708 . . . . . . . 8
2917simp3bi 1047 . . . . . . . . . . . . 13
3022, 29bnj835 29642 . . . . . . . . . . . 12
31 eluni2 4194 . . . . . . . . . . . . . 14
3231biimpi 199 . . . . . . . . . . . . 13
3332bnj1196 29678 . . . . . . . . . . . 12
3430, 33syl 17 . . . . . . . . . . 11
35 bnj1379.7 . . . . . . . . . . 11
36 nfv 1769 . . . . . . . . . . . . . . . . . 18
37 nfra2 2790 . . . . . . . . . . . . . . . . . 18
3836, 37nfan 2031 . . . . . . . . . . . . . . . . 17
391, 38nfxfr 1704 . . . . . . . . . . . . . . . 16
40 nfv 1769 . . . . . . . . . . . . . . . 16
41 nfv 1769 . . . . . . . . . . . . . . . 16
4239, 40, 41nf3an 2033 . . . . . . . . . . . . . . 15
4317, 42nfxfr 1704 . . . . . . . . . . . . . 14
44 nfv 1769 . . . . . . . . . . . . . 14
45 nfv 1769 . . . . . . . . . . . . . 14
4643, 44, 45nf3an 2033 . . . . . . . . . . . . 13
4722, 46nfxfr 1704 . . . . . . . . . . . 12
4847nfri 1972 . . . . . . . . . . 11
4934, 35, 48bnj1345 29708 . . . . . . . . . 10
501simprbi 471 . . . . . . . . . . . . . . . . . 18
5117, 50bnj835 29642 . . . . . . . . . . . . . . . . 17
5222, 51bnj835 29642 . . . . . . . . . . . . . . . 16
5335, 52bnj835 29642 . . . . . . . . . . . . . . 15
5422, 35bnj1219 29684 . . . . . . . . . . . . . . 15
5553, 54bnj1294 29701 . . . . . . . . . . . . . 14
5635simp2bi 1046 . . . . . . . . . . . . . 14
5755, 56bnj1294 29701 . . . . . . . . . . . . 13
5857fveq1d 5881 . . . . . . . . . . . 12
5922simp3bi 1047 . . . . . . . . . . . . . . . . 17
6035, 59bnj835 29642 . . . . . . . . . . . . . . . 16
61 vex 3034 . . . . . . . . . . . . . . . . 17
62 vex 3034 . . . . . . . . . . . . . . . . 17
6361, 62opeldm 5044 . . . . . . . . . . . . . . . 16
6460, 63syl 17 . . . . . . . . . . . . . . 15
65 vex 3034 . . . . . . . . . . . . . . . . 17
6661, 65opeldm 5044 . . . . . . . . . . . . . . . 16
6735, 66bnj837 29644 . . . . . . . . . . . . . . 15
6864, 67elind 3609 . . . . . . . . . . . . . 14
69 bnj1379.2 . . . . . . . . . . . . . 14
7068, 69syl6eleqr 2560 . . . . . . . . . . . . 13
71 fvres 5893 . . . . . . . . . . . . 13
7270, 71syl 17 . . . . . . . . . . . 12
73 fvres 5893 . . . . . . . . . . . . 13
7470, 73syl 17 . . . . . . . . . . . 12
7558, 72, 743eqtr3d 2513 . . . . . . . . . . 11
762biimpi 199 . . . . . . . . . . . . . . . . 17
771, 76bnj832 29640 . . . . . . . . . . . . . . . 16
7817, 77bnj835 29642 . . . . . . . . . . . . . . 15
7922, 78bnj835 29642 . . . . . . . . . . . . . 14
8035, 79bnj835 29642 . . . . . . . . . . . . 13
8180, 54bnj1294 29701 . . . . . . . . . . . 12
82 funopfv 5918 . . . . . . . . . . . 12
8381, 60, 82sylc 61 . . . . . . . . . . 11
84 funeq 5608 . . . . . . . . . . . . . . 15
8584cbvralv 3005 . . . . . . . . . . . . . 14
8680, 85sylib 201 . . . . . . . . . . . . 13
8786, 56bnj1294 29701 . . . . . . . . . . . 12
8835simp3bi 1047 . . . . . . . . . . . 12
89 funopfv 5918 . . . . . . . . . . . 12
9087, 88, 89sylc 61 . . . . . . . . . . 11
9175, 83, 903eqtr3d 2513 . . . . . . . . . 10
9249, 91bnj593 29627 . . . . . . . . 9
9392bnj937 29655 . . . . . . . 8
9428, 93bnj593 29627 . . . . . . 7
9594bnj937 29655 . . . . . 6
9617, 95sylbir 218 . . . . 5
97963expib 1234 . . . 4
9897alrimivv 1782 . . 3
9998alrimiv 1781 . 2
100 dffun4 5601 . 2
10116, 99, 100sylanbrc 677 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   w3a 1007  wal 1450   wceq 1452  wex 1671   wcel 1904  wral 2756  wrex 2757   cin 3389  cop 3965  cuni 4190   cdm 4839   cres 4841   wrel 4844   wfun 5583  cfv 5589 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-iun 4271  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-res 4851  df-iota 5553  df-fun 5591  df-fv 5597 This theorem is referenced by:  bnj1383  29715
 Copyright terms: Public domain W3C validator