ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rabxfrd Structured version   Unicode version

Theorem rabxfrd 4167
Description: Class builder membership after substituting an expression (containing ) for in the class expression . (Contributed by NM, 16-Jan-2012.)
Hypotheses
Ref Expression
rabxfrd.1  F/_
rabxfrd.2  F/_ C
rabxfrd.3  D  D
rabxfrd.4
rabxfrd.5  C
Assertion
Ref Expression
rabxfrd  D  C 
{  D  |  }  {  D  |  }
Distinct variable groups:   ,   ,, D   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()   (,)    C(,)

Proof of Theorem rabxfrd
StepHypRef Expression
1 rabxfrd.3 . . . . . . . . . . 11  D  D
21ex 108 . . . . . . . . . 10  D  D
3 ibibr 235 . . . . . . . . . 10  D  D  D  D  D
42, 3sylib 127 . . . . . . . . 9  D  D  D
54imp 115 . . . . . . . 8  D  D  D
65anbi1d 438 . . . . . . 7  D  D  D
7 rabxfrd.4 . . . . . . . 8
87elrab 2692 . . . . . . 7  {  D  |  }  D
9 rabid 2479 . . . . . . 7  {  D  |  }  D
106, 8, 93bitr4g 212 . . . . . 6  D  {  D  |  }  {  D  |  }
1110rabbidva 2542 . . . . 5  {  D  |  {  D  |  } }  {  D  |  {  D  |  } }
1211eleq2d 2104 . . . 4  {  D  |  {  D  |  } }  {  D  |  {  D  |  } }
13 rabxfrd.1 . . . . 5  F/_
14 nfcv 2175 . . . . 5  F/_ D
15 rabxfrd.2 . . . . . 6  F/_ C
1615nfel1 2185 . . . . 5  F/  C  {  D  |  }
17 rabxfrd.5 . . . . . 6  C
1817eleq1d 2103 . . . . 5  {  D  |  }  C  {  D  |  }
1913, 14, 16, 18elrabf 2690 . . . 4  {  D  |  {  D  |  } }  D  C  {  D  |  }
20 nfrab1 2483 . . . . . 6  F/_ {  D  |  }
2113, 20nfel 2183 . . . . 5  F/  {  D  |  }
22 eleq1 2097 . . . . 5  {  D  |  }  {  D  |  }
2313, 14, 21, 22elrabf 2690 . . . 4  {  D  | 
{  D  |  } }  D  {  D  |  }
2412, 19, 233bitr3g 211 . . 3  D  C  {  D  |  }  D  {  D  |  }
25 pm5.32 426 . . 3  D  C  {  D  |  }  {  D  |  }  D  C  {  D  |  }  D  {  D  |  }
2624, 25sylibr 137 . 2  D  C  {  D  |  }  {  D  |  }
2726imp 115 1  D  C 
{  D  |  }  {  D  |  }
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98   wceq 1242   wcel 1390   F/_wnfc 2162   {crab 2304
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rab 2309  df-v 2553
This theorem is referenced by:  rabxfr  4168
  Copyright terms: Public domain W3C validator