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

Theorem bnj1154 32833
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 32586 . 2
2 elisset 3092 . . . . 5
32bnj708 32591 . . . 4
4 df-fr 4796 . . . . . . . 8
54biimpi 194 . . . . . . 7
6519.21bi 1809 . . . . . 6
763impib 1186 . . . . 5
8 sseq1 3491 . . . . . . 7
9 neeq1 2734 . . . . . . 7
108, 93anbi23d 1293 . . . . . 6
11 raleq 3026 . . . . . . 7
1211rexeqbi1dv 3035 . . . . . 6
1310, 12imbi12d 320 . . . . 5
147, 13mpbii 211 . . . 4
153, 14bnj593 32580 . . 3
1615bnj937 32608 . 2
171, 16mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369  /\w3a 965  A.wal 1368  =wceq 1370  E.wex 1587  e.wcel 1758  =/=wne 2648  A.wral 2800  E.wrex 2801   cvv 3081  C_wss 3442   c0 3751   class class class wbr 4409  Frwfr 4793  /\w-bnj17 32517
This theorem is referenced by:  bnj1190  32842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2805  df-rex 2806  df-v 3083  df-in 3449  df-ss 3456  df-fr 4796  df-bnj17 32518
  Copyright terms: Public domain W3C validator