ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elrab GIF version

Theorem elrab 2893
Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.)
Hypothesis
Ref Expression
elrab.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
elrab (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrab
StepHypRef Expression
1 nfcv 2319 . 2 𝑥𝐴
2 nfcv 2319 . 2 𝑥𝐵
3 nfv 1528 . 2 𝑥𝜓
4 elrab.1 . 2 (𝑥 = 𝐴 → (𝜑𝜓))
51, 2, 3, 4elrabf 2891 1 (𝐴 ∈ {𝑥𝐵𝜑} ↔ (𝐴𝐵𝜓))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  {crab 2459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2739
This theorem is referenced by:  elrab3  2894  elrabd  2895  elrab2  2896  ralrab  2898  rexrab  2900  rabsnt  3666  unimax  3841  ssintub  3860  intminss  3867  exmidexmid  4193  exmidsssnc  4200  rabxfrd  4466  ordtri2or2exmidlem  4522  onsucelsucexmidlem1  4524  sefvex  5532  ssimaex  5573  acexmidlem2  5866  elpmg  6658  ssfilem  6869  diffitest  6881  inffiexmid  6900  supubti  6992  suplubti  6993  ctssexmid  7142  exmidonfinlem  7186  cc4f  7259  cc4n  7261  caucvgprlemladdfu  7667  caucvgprlemladdrl  7668  suplocexprlemmu  7708  suplocexprlemru  7709  suplocexprlemdisj  7710  suplocexprlemub  7713  nnindnn  7883  negf1o  8329  apsscn  8594  sup3exmid  8903  nnind  8924  peano2uz2  9349  peano5uzti  9350  dfuzi  9352  uzind  9353  uzind3  9355  eluz1  9521  uzind4  9577  supinfneg  9584  infsupneg  9585  eqreznegel  9603  elixx1  9884  elioo2  9908  elfz1  10000  expcl2lemap  10518  expclzaplem  10530  expclzap  10531  expap0i  10538  expge0  10542  expge1  10543  hashennnuni  10743  shftf  10823  reccn2ap  11305  dvdsdivcl  11839  divalgmod  11915  zsupcl  11931  infssuzex  11933  infssuzcldc  11935  bezoutlemsup  11993  dfgcd2  11998  uzwodc  12021  nnwosdc  12023  lcmcllem  12050  lcmledvds  12053  lcmgcdlem  12060  1nprm  12097  1idssfct  12098  isprm2  12100  phicl2  12197  hashdvds  12204  phisum  12223  odzval  12224  odzcllem  12225  odzdvds  12228  oddennn  12376  evenennn  12377  znnen  12382  ennnfonelemg  12387  ennnfonelemom  12392  ismhm  12743  issubm  12753  issubmd  12755  grplinv  12812  istopon  13178  epttop  13257  iscld  13270  isnei  13311  neipsm  13321  iscn  13364  iscnp  13366  txdis1cn  13445  ishmeo  13471  ispsmet  13490  ismet  13511  isxmet  13512  elblps  13557  elbl  13558  xmetxpbl  13675  reopnap  13705  divcnap  13722  elcncf  13727  cdivcncfap  13754  cnopnap  13761  ellimc3apf  13796  limccoap  13814  dvlemap  13816  dvidlemap  13827  dvcnp2cntop  13830  dvaddxxbr  13832  dvmulxxbr  13833  dvcoapbr  13838  dvcjbr  13839  dvrecap  13844  dveflem  13854  lgsfle1  14077  lgsle1  14083  lgsdirprm  14102  lgsne0  14106  subctctexmid  14406
  Copyright terms: Public domain W3C validator