Theorem elrab 2973

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2203  {crab 2524

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rab 2529  df-v 2815

This theorem is referenced by:  elrab3  2974  elrabd  2975  elrab2  2976  ralrab  2978  rexrab  2980  rabsnt  3766  unimax  3948  ssintub  3967  intminss  3974  exmidexmid  4309  exmidsssnc  4316  rabxfrd  4590  ordtri2or2exmidlem  4648  onsucelsucexmidlem1  4650  sefvex  5691  ssimaex  5738  acexmidlem2  6047  elsuppfng  6442  elsuppfn  6443  elpmg  6898  ssfilem  7130  ssfilemd  7132  diffitest  7144  inffiexmid  7166  2omap  7269  supubti  7290  suplubti  7291  ctssexmid  7441  sspw1or2  7495  exmidonfinlem  7496  finacn  7511  cc4f  7583  cc4n  7585  acnccim  7586  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemdisj  8035  suplocexprlemub  8038  nnindnn  8208  negf1o  8655  apsscn  8921  sup3exmid  9231  nnind  9253  peano2uz2  9685  peano5uzti  9686  dfuzi  9688  uzind  9689  uzind3  9691  eluz1  9857  uzind4  9920  supinfneg  9927  infsupneg  9928  eqreznegel  9946  elixx1  10230  elioo2  10254  elfz1  10347  zsupcl  10591  infssuzex  10593  infssuzcldc  10595  expcl2lemap  10913  expclzaplem  10925  expclzap  10926  expap0i  10933  expge0  10937  expge1  10938  hashennnuni  11142  hashfibclem  11206  wrdmap  11256  shftf  11515  reccn2ap  11998  dvdsdivcl  12536  divalgmod  12613  bitsval  12629  bitsfzolem  12640  bezoutlemsup  12705  dfgcd2  12710  uzwodc  12733  nnwosdc  12735  nninfctlemfo  12736  lcmgcdlem  12774  1nprm  12811  1idssfct  12812  isprm2  12814  phicl2  12911  hashdvds  12918  dvdsfi  12936  phisum  12938  odzval  12939  odzcllem  12940  odzdvds  12943  oddennn  13143  evenennn  13144  znnen  13149  ennnfonelemg  13154  ennnfonelemom  13159  ismhm  13674  issubm  13685  issubmd  13687  grplinv  13763  issubg  13890  isnsg  13919  isrim0  14306  issubrng  14344  issubrg  14366  islssm  14505  islssmg  14506  cnfldui  14737  mplelbascoe  14847  istopon  14878  epttop  14955  iscld  14968  isnei  15009  neipsm  15019  iscn  15062  iscnp  15064  txdis1cn  15143  ishmeo  15169  ispsmet  15188  ismet  15209  isxmet  15210  elblps  15255  elbl  15256  xmetxpbl  15373  reopnap  15411  divcnap  15430  elcncf  15438  cdivcncfap  15469  cnopnap  15476  divcncfap  15479  maxcncf  15480  mincncf  15481  ellimc3apf  15525  limccoap  15543  dvlemap  15545  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvcnp2cntop  15564  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  dvrecap  15578  dveflem  15591  pellexlem3  15847  dvdsppwf1o  15857  lgsfle1  15882  lgsle1  15888  lgsdirprm  15907  lgsne0  15911  lgsquadlem1  15950  lgsquadlem2  15951  uhgrm  16073  upgrm  16095  upgr1or2  16096  umgredg2en  16104  umgrbien  16105  uhgredgm  16131  edgupgren  16136  edgumgren  16137  edgusgren  16158  usgruspgrben  16181  ushgredgedg  16221  ushgredgedgloop  16223  isclwwlk  16389  isclwwlkng  16401  clwwlknon  16424  eupth2lemsfi  16473  konigsberglem1  16483  konigsberglem4  16486  pw1map  16769  subctctexmid  16774