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

Theorem bnj101 32555
Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj101.1
bnj101.2
Assertion
Ref Expression
bnj101

Proof of Theorem bnj101
StepHypRef Expression
1 bnj101.1 . 2
2 bnj101.2 . 2
31, 2eximii 1628 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  E.wex 1587
This theorem is referenced by:  bnj1023  32617  bnj1098  32620  bnj1101  32621  bnj1109  32623  bnj1468  32682  bnj1014  32796  bnj907  32801  bnj1110  32816  bnj1118  32818  bnj1128  32824  bnj1145  32827  bnj1172  32835  bnj1174  32837  bnj1176  32839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-ex 1588
  Copyright terms: Public domain W3C validator