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

Theorem fpwwe2lem1 8790
 Description: Lemma for fpwwe2 8802. (Contributed by Mario Carneiro, 15-May-2015.)
Hypothesis
Ref Expression
fpwwe2.1
Assertion
Ref Expression
fpwwe2lem1
Distinct variable groups:   ,,,,   ,,   ,,,,
Allowed substitution hints:   (,)

Proof of Theorem fpwwe2lem1
StepHypRef Expression
1 simpll 753 . . . . 5
2 selpw 3862 . . . . 5
31, 2sylibr 212 . . . 4
4 simplr 754 . . . . . 6
5 xpss12 4940 . . . . . . 7
61, 1, 5syl2anc 661 . . . . . 6
74, 6sstrd 3361 . . . . 5
8 selpw 3862 . . . . 5
97, 8sylibr 212 . . . 4
103, 9jca 532 . . 3
1110ssopab2i 4611 . 2
12 fpwwe2.1 . 2
13 df-xp 4841 . 2
1411, 12, 133sstr4i 3390 1
 Colors of variables: wff setvar class Syntax hints:   wa 369   wceq 1369   wcel 1756  wral 2710  wsbc 3181   cin 3322   wss 3323  cpw 3855  csn 3872  copab 4344   wwe 4673   cxp 4833  ccnv 4834  cima 4838  (class class class)co 6086 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337  df-pw 3857  df-opab 4346  df-xp 4841 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator