Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  el2v Structured version   Visualization version   GIF version

Theorem el2v 34329
Description: New way (elv 34328, and the theorems beginning with "el2v" or "el3v") to shorten some proofs. Inference forms (with 𝐴 ∈ V and 𝐵 ∈ V hypotheses) of the general theorems (proving ((𝐴𝑉𝐵𝑊) → assertions) may be superfluous. (Contributed by Peter Mazsa, 13-Oct-2018.)
Hypothesis
Ref Expression
el2v.1 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)
Assertion
Ref Expression
el2v 𝜑

Proof of Theorem el2v
StepHypRef Expression
1 vex 3354 . 2 𝑥 ∈ V
2 vex 3354 . 2 𝑦 ∈ V
3 el2v.1 . 2 ((𝑥 ∈ V ∧ 𝑦 ∈ V) → 𝜑)
41, 2, 3mp2an 672 1 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 2145  Vcvv 3351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-tru 1634  df-ex 1853  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-v 3353
This theorem is referenced by:  vvdifopab  34367  inxprnres  34403  ineccnvmo  34464  alrmomorn  34465  dfcoss2  34513  dfcoss3  34514  cocossss  34533  cnvcosseq  34534  rncossdmcoss  34547  symrelcoss3  34557  1cosscnvxrn  34567  cosscnvssid3  34568  cosscnvssid4  34569  coss0  34571  trcoss  34574  trcoss2  34576
  Copyright terms: Public domain W3C validator