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  7485  caucvgprlemladdrl  7486  suplocexprlemmu  7526  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemub  7531  nnindnn  7701  negf1o  8144  apsscn  8409  sup3exmid  8715  nnind  8736  peano2uz2  9158  peano5uzti  9159  dfuzi  9161  uzind  9162  uzind3  9164  eluz1  9330  uzind4  9383  supinfneg  9390  infsupneg  9391  eqreznegel  9406  elixx1  9680  elioo2  9704  elfz1  9795  expcl2lemap  10305  expclzaplem  10317  expclzap  10318  expap0i  10325  expge0  10329  expge1  10330  hashennnuni  10525  shftf  10602  reccn2ap  11082  dvdsdivcl  11548  divalgmod  11624  zsupcl  11640  infssuzex  11642  infssuzcldc  11644  bezoutlemsup  11697  dfgcd2  11702  lcmcllem  11748  lcmledvds  11751  lcmgcdlem  11758  1nprm  11795  1idssfct  11796  isprm2  11798  phicl2  11890  hashdvds  11897  oddennn  11905  evenennn  11906  znnen  11911  ennnfonelemg  11916  ennnfonelemom  11921  istopon  12180  epttop  12259  iscld  12272  isnei  12313  neipsm  12323  iscn  12366  iscnp  12368  txdis1cn  12447  ishmeo  12473  ispsmet  12492  ismet  12513  isxmet  12514  elblps  12559  elbl  12560  xmetxpbl  12677  reopnap  12707  divcnap  12724  elcncf  12729  cdivcncfap  12756  cnopnap  12763  ellimc3apf  12798  limccoap  12816  dvlemap  12818  dvidlemap  12829  dvcnp2cntop  12832  dvaddxxbr  12834  dvmulxxbr  12835  dvcoapbr  12840  dvcjbr  12841  dvrecap  12846  dveflem  12855  subctctexmid  13196