Theorem elrab 2982

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 2392	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2392	. 2 ⊢ Ⅎ𝑥𝐵
3		nfv 1581	. 2 ⊢ Ⅎ𝑥𝜓
4		elrab.1	. 2 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	elrabf 2980	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {crab 2532

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823

This theorem is referenced by:  elrab3  2983  elrabd  2984  elrab2  2985  ralrab  2987  rexrab  2989  rabsnt  3782  unimax  3964  ssintub  3983  intminss  3990  exmidexmid  4328  exmidsssnc  4335  rabxfrd  4610  ordtri2or2exmidlem  4668  onsucelsucexmidlem1  4670  sefvex  5711  ssimaex  5758  acexmidlem2  6072  elsuppfng  6472  elsuppfn  6473  elpmg  6928  ssfilem  7167  ssfilemd  7169  diffitest  7181  inffiexmid  7203  2omap  7308  supubti  7329  suplubti  7330  ctssexmid  7480  sspw1or2  7534  exmidonfinlem  7535  finacn  7550  cc4f  7625  cc4n  7627  acnccim  7628  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemdisj  8077  suplocexprlemub  8080  nnindnn  8250  negf1o  8699  apsscn  8965  sup3exmid  9277  nnind  9299  peano2uz2  9732  peano5uzti  9733  dfuzi  9735  uzind  9736  uzind3  9738  eluz1  9904  uzind4  9967  supinfneg  9974  infsupneg  9975  eqreznegel  9993  elixx1  10278  elioo2  10302  elfz1  10395  zsupcl  10642  infssuzex  10644  infssuzcldc  10646  expcl2lemap  10966  expclzaplem  10978  expclzap  10979  expap0i  10986  expge0  10990  expge1  10991  hashennnuni  11196  hashfibclem  11260  wrdmap  11314  shftf  11573  reccn2ap  12057  dvdsdivcl  12595  divalgmod  12672  bitsval  12688  bitsfzolem  12699  bezoutlemsup  12764  dfgcd2  12769  uzwodc  12792  nnwosdc  12794  nninfctlemfo  12795  lcmgcdlem  12833  1nprm  12870  1idssfct  12871  isprm2  12873  phicl2  12970  hashdvds  12977  dvdsfi  12995  phisum  12997  odzval  12998  odzcllem  12999  odzdvds  13002  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemiex  13222  ballotfilemimin  13227  ballotfilemfrcn0  13251  ballotfilemirc  13253  ballotfilem7  13257  oddennn  13261  evenennn  13262  znnen  13267  ennnfonelemg  13272  ennnfonelemom  13277  ismhm  13745  issubm  13756  issubmd  13758  grplinv  13832  issubg  13953  isnsg  13982  isrim0  14441  issubrng  14480  issubrg  14502  ringunitsap0  14567  drnguiap  14582  islssm  14666  islssmg  14667  cnfldui  14896  mplelbascoe  15006  istopon  15037  epttop  15114  iscld  15127  isnei  15168  neipsm  15178  iscn  15221  iscnp  15223  txdis1cn  15302  ishmeo  15328  ispsmet  15347  ismet  15368  isxmet  15369  elblps  15414  elbl  15415  xmetxpbl  15532  reopnap  15570  divcnap  15589  elcncf  15597  cdivcncfap  15628  cnopnap  15635  divcncfap  15638  maxcncf  15639  mincncf  15640  ellimc3apf  15684  limccoap  15702  dvlemap  15704  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvrecap  15737  dveflem  15750  pellexlem3  16007  dvdsppwf1o  16017  lgsfle1  16042  lgsle1  16048  lgsdirprm  16067  lgsne0  16071  lgsquadlem1  16110  lgsquadlem2  16111  uhgrm  16233  upgrm  16255  upgr1or2  16256  umgredg2en  16264  umgrbien  16265  uhgredgm  16291  edgupgren  16296  edgumgren  16297  edgusgren  16318  usgruspgrben  16341  ushgredgedg  16381  ushgredgedgloop  16383  isclwwlk  16549  isclwwlkng  16561  clwwlknon  16584  eupth2lemsfi  16633  konigsberglem1  16643  konigsberglem4  16646  pw1map  16939  subctctexmid  16944