Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1154 Unicode version

Theorem bnj1154 31568
Description: Property of Fr. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
bnj1154
Distinct variable groups:   , ,   , ,   , ,

Proof of Theorem bnj1154
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 bnj658 31321 . 2
2 elisset 2962 . . . . 5
32bnj708 31326 . . . 4
4 df-fr 4650 . . . . . . . 8
54biimpi 188 . . . . . . 7
6519.21bi 1797 . . . . . 6
763impib 1170 . . . . 5
8 sseq1 3354 . . . . . . 7
9 neeq1 2595 . . . . . . 7
108, 93anbi23d 1277 . . . . . 6
11 raleq 2896 . . . . . . 7
1211rexeqbi1dv 2905 . . . . . 6
1310, 12imbi12d 314 . . . . 5
147, 13mpbii 205 . . . 4
153, 14bnj593 31315 . . 3
1615bnj937 31343 . 2
171, 16mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 362  /\w3a 950  A.wal 1580  E.wex 1581  =wceq 1687  e.wcel 1749  =/=wne 2585  A.wral 2694  E.wrex 2695   cvv 2951  C_wss 3305   c0 3614   class class class wbr 4267  Frwfr 4647  /\w-bnj17 31252
This theorem is referenced by:  bnj1190  31577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-ral 2699  df-rex 2700  df-v 2953  df-in 3312  df-ss 3319  df-fr 4650  df-bnj17 31253
  Copyright terms: Public domain W3C validator