Theorem elrab 2840

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331   ∈ wcel 1480  {crab 2420

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rab 2425  df-v 2688

This theorem is referenced by:  elrab3  2841  elrabd  2842  elrab2  2843  ralrab  2845  rexrab  2847  rabsnt  3598  unimax  3770  ssintub  3789  intminss  3796  exmidexmid  4120  exmidsssnc  4126  rabxfrd  4390  ordtri2or2exmidlem  4441  onsucelsucexmidlem1  4443  sefvex  5442  ssimaex  5482  acexmidlem2  5771  elpmg  6558  ssfilem  6769  diffitest  6781  inffiexmid  6800  supubti  6886  suplubti  6887  ctssexmid  7024  exmidonfinlem  7049  caucvgprlemladdfu  7488  caucvgprlemladdrl  7489  suplocexprlemmu  7529  suplocexprlemru  7530  suplocexprlemdisj  7531  suplocexprlemub  7534  nnindnn  7704  negf1o  8147  apsscn  8412  sup3exmid  8718  nnind  8739  peano2uz2  9161  peano5uzti  9162  dfuzi  9164  uzind  9165  uzind3  9167  eluz1  9333  uzind4  9386  supinfneg  9393  infsupneg  9394  eqreznegel  9409  elixx1  9683  elioo2  9707  elfz1  9798  expcl2lemap  10308  expclzaplem  10320  expclzap  10321  expap0i  10328  expge0  10332  expge1  10333  hashennnuni  10528  shftf  10605  reccn2ap  11085  dvdsdivcl  11551  divalgmod  11627  zsupcl  11643  infssuzex  11645  infssuzcldc  11647  bezoutlemsup  11700  dfgcd2  11705  lcmcllem  11751  lcmledvds  11754  lcmgcdlem  11761  1nprm  11798  1idssfct  11799  isprm2  11801  phicl2  11893  hashdvds  11900  oddennn  11908  evenennn  11909  znnen  11914  ennnfonelemg  11919  ennnfonelemom  11924  istopon  12183  epttop  12262  iscld  12275  isnei  12316  neipsm  12326  iscn  12369  iscnp  12371  txdis1cn  12450  ishmeo  12476  ispsmet  12495  ismet  12516  isxmet  12517  elblps  12562  elbl  12563  xmetxpbl  12680  reopnap  12710  divcnap  12727  elcncf  12732  cdivcncfap  12759  cnopnap  12766  ellimc3apf  12801  limccoap  12819  dvlemap  12821  dvidlemap  12832  dvcnp2cntop  12835  dvaddxxbr  12837  dvmulxxbr  12838  dvcoapbr  12843  dvcjbr  12844  dvrecap  12849  dveflem  12858  subctctexmid  13199