Theorem elrab 2960

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

Step	Hyp	Ref	Expression
1		nfcv 2372	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2372	. 2 ⊢ Ⅎ𝑥𝐵
3		nfv 1574	. 2 ⊢ Ⅎ𝑥𝜓
4		elrab.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	elrabf 2958	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  {crab 2512

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rab 2517  df-v 2802

This theorem is referenced by:  elrab3  2961  elrabd  2962  elrab2  2963  ralrab  2965  rexrab  2967  rabsnt  3744  unimax  3925  ssintub  3944  intminss  3951  exmidexmid  4284  exmidsssnc  4291  rabxfrd  4564  ordtri2or2exmidlem  4622  onsucelsucexmidlem1  4624  sefvex  5656  ssimaex  5703  acexmidlem2  6010  elpmg  6828  ssfilem  7057  diffitest  7069  inffiexmid  7091  supubti  7189  suplubti  7190  ctssexmid  7340  exmidonfinlem  7394  finacn  7409  cc4f  7478  cc4n  7480  acnccim  7481  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemub  7933  nnindnn  8103  negf1o  8551  apsscn  8817  sup3exmid  9127  nnind  9149  peano2uz2  9577  peano5uzti  9578  dfuzi  9580  uzind  9581  uzind3  9583  eluz1  9749  uzind4  9812  supinfneg  9819  infsupneg  9820  eqreznegel  9838  elixx1  10122  elioo2  10146  elfz1  10238  zsupcl  10481  infssuzex  10483  infssuzcldc  10485  expcl2lemap  10803  expclzaplem  10815  expclzap  10816  expap0i  10823  expge0  10827  expge1  10828  hashennnuni  11031  wrdmap  11135  shftf  11381  reccn2ap  11864  dvdsdivcl  12401  divalgmod  12478  bitsval  12494  bitsfzolem  12505  bezoutlemsup  12570  dfgcd2  12575  uzwodc  12598  nnwosdc  12600  nninfctlemfo  12601  lcmgcdlem  12639  1nprm  12676  1idssfct  12677  isprm2  12679  phicl2  12776  hashdvds  12783  dvdsfi  12801  phisum  12803  odzval  12804  odzcllem  12805  odzdvds  12808  oddennn  13003  evenennn  13004  znnen  13009  ennnfonelemg  13014  ennnfonelemom  13019  ismhm  13534  issubm  13545  issubmd  13547  grplinv  13623  issubg  13750  isnsg  13779  isrim0  14165  issubrng  14203  issubrg  14225  islssm  14361  islssmg  14362  cnfldui  14593  mplelbascoe  14696  istopon  14727  epttop  14804  iscld  14817  isnei  14858  neipsm  14868  iscn  14911  iscnp  14913  txdis1cn  14992  ishmeo  15018  ispsmet  15037  ismet  15058  isxmet  15059  elblps  15104  elbl  15105  xmetxpbl  15222  reopnap  15260  divcnap  15279  elcncf  15287  cdivcncfap  15318  cnopnap  15325  divcncfap  15328  maxcncf  15329  mincncf  15330  ellimc3apf  15374  limccoap  15392  dvlemap  15394  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  dvrecap  15427  dveflem  15440  dvdsppwf1o  15703  lgsfle1  15728  lgsle1  15734  lgsdirprm  15753  lgsne0  15757  lgsquadlem1  15796  lgsquadlem2  15797  uhgrm  15919  upgrm  15941  upgr1or2  15942  umgredg2en  15950  umgrbien  15951  uhgredgm  15975  edgupgren  15980  edgumgren  15981  edgusgren  16002  usgruspgrben  16025  ushgredgedg  16065  ushgredgedgloop  16067  isclwwlk  16189  isclwwlkng  16201  clwwlknon  16224  2omap  16530  pw1map  16532  subctctexmid  16537