MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elmpt2cl Unicode version

Theorem elmpt2cl 6517
Description: If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015.)
Hypothesis
Ref Expression
elmpt2cl.f
Assertion
Ref Expression
elmpt2cl
Distinct variable groups:   , ,   , ,

Proof of Theorem elmpt2cl
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elmpt2cl.f . . . . . 6
2 df-mpt2 6301 . . . . . 6
31, 2eqtri 2486 . . . . 5
43dmeqi 5209 . . . 4
5 dmoprabss 6384 . . . 4
64, 5eqsstri 3533 . . 3
7 elfvdm 5897 . . . 4
8 df-ov 6299 . . . 4
97, 8eleq2s 2565 . . 3
106, 9sseldi 3501 . 2
11 opelxp 5034 . 2
1210, 11sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  e.wcel 1818  <.cop 4035  X.cxp 5002  domcdm 5004  `cfv 5593  (class class class)co 6296  {coprab 6297  e.cmpt2 6298
This theorem is referenced by:  elmpt2cl1  6518  elmpt2cl2  6519  elovmpt2  6520  elovmpt2rab  6521  elovmpt2rab1  6522  ixxssixx  11572  funcrcl  15232  natrcl  15319  ismhm  15968  isghm  16267  isga  16329  isslw  16628  isrhm  17370  rimrcl  17373  islmhm  17673  iscn2  19739  elflim2  20465  isfcls  20510  isnmhm  21253  limcrcl  22278  clwlkswlks  24758  clwwlkprop  24770  iscvm  28704  mclsrcl  28921  mgmhmrcl  32469  intop  32527  rnghmrcl  32695  rngimrcl  32703
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-xp 5010  df-dm 5014  df-iota 5556  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301
  Copyright terms: Public domain W3C validator