Theorem elrab 2962

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1397   ∈ wcel 2202  {crab 2514

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rab 2519  df-v 2804

This theorem is referenced by:  elrab3  2963  elrabd  2964  elrab2  2965  ralrab  2967  rexrab  2969  rabsnt  3746  unimax  3927  ssintub  3946  intminss  3953  exmidexmid  4286  exmidsssnc  4293  rabxfrd  4566  ordtri2or2exmidlem  4624  onsucelsucexmidlem1  4626  sefvex  5660  ssimaex  5707  acexmidlem2  6014  elpmg  6832  ssfilem  7061  ssfilemd  7063  diffitest  7075  inffiexmid  7097  supubti  7197  suplubti  7198  ctssexmid  7348  sspw1or2  7402  exmidonfinlem  7403  finacn  7418  cc4f  7487  cc4n  7489  acnccim  7490  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemub  7942  nnindnn  8112  negf1o  8560  apsscn  8826  sup3exmid  9136  nnind  9158  peano2uz2  9586  peano5uzti  9587  dfuzi  9589  uzind  9590  uzind3  9592  eluz1  9758  uzind4  9821  supinfneg  9828  infsupneg  9829  eqreznegel  9847  elixx1  10131  elioo2  10155  elfz1  10247  zsupcl  10490  infssuzex  10492  infssuzcldc  10494  expcl2lemap  10812  expclzaplem  10824  expclzap  10825  expap0i  10832  expge0  10836  expge1  10837  hashennnuni  11040  wrdmap  11144  shftf  11390  reccn2ap  11873  dvdsdivcl  12410  divalgmod  12487  bitsval  12503  bitsfzolem  12514  bezoutlemsup  12579  dfgcd2  12584  uzwodc  12607  nnwosdc  12609  nninfctlemfo  12610  lcmgcdlem  12648  1nprm  12685  1idssfct  12686  isprm2  12688  phicl2  12785  hashdvds  12792  dvdsfi  12810  phisum  12812  odzval  12813  odzcllem  12814  odzdvds  12817  oddennn  13012  evenennn  13013  znnen  13018  ennnfonelemg  13023  ennnfonelemom  13028  ismhm  13543  issubm  13554  issubmd  13556  grplinv  13632  issubg  13759  isnsg  13788  isrim0  14174  issubrng  14212  issubrg  14234  islssm  14370  islssmg  14371  cnfldui  14602  mplelbascoe  14705  istopon  14736  epttop  14813  iscld  14826  isnei  14867  neipsm  14877  iscn  14920  iscnp  14922  txdis1cn  15001  ishmeo  15027  ispsmet  15046  ismet  15067  isxmet  15068  elblps  15113  elbl  15114  xmetxpbl  15231  reopnap  15269  divcnap  15288  elcncf  15296  cdivcncfap  15327  cnopnap  15334  divcncfap  15337  maxcncf  15338  mincncf  15339  ellimc3apf  15383  limccoap  15401  dvlemap  15403  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  dvrecap  15436  dveflem  15449  dvdsppwf1o  15712  lgsfle1  15737  lgsle1  15743  lgsdirprm  15762  lgsne0  15766  lgsquadlem1  15805  lgsquadlem2  15806  uhgrm  15928  upgrm  15950  upgr1or2  15951  umgredg2en  15959  umgrbien  15960  uhgredgm  15986  edgupgren  15991  edgumgren  15992  edgusgren  16013  usgruspgrben  16036  ushgredgedg  16076  ushgredgedgloop  16078  isclwwlk  16244  isclwwlkng  16256  clwwlknon  16279  2omap  16594  pw1map  16596  subctctexmid  16601