Theorem elrab 2864

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

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1332   ∈ wcel 2125  {crab 2436

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-rab 2441  df-v 2711

This theorem is referenced by:  elrab3  2865  elrabd  2866  elrab2  2867  ralrab  2869  rexrab  2871  rabsnt  3630  unimax  3802  ssintub  3821  intminss  3828  exmidexmid  4152  exmidsssnc  4159  rabxfrd  4423  ordtri2or2exmidlem  4479  onsucelsucexmidlem1  4481  sefvex  5482  ssimaex  5522  acexmidlem2  5811  elpmg  6598  ssfilem  6809  diffitest  6821  inffiexmid  6840  supubti  6931  suplubti  6932  ctssexmid  7072  exmidonfinlem  7107  cc4f  7168  cc4n  7170  caucvgprlemladdfu  7576  caucvgprlemladdrl  7577  suplocexprlemmu  7617  suplocexprlemru  7618  suplocexprlemdisj  7619  suplocexprlemub  7622  nnindnn  7792  negf1o  8236  apsscn  8501  sup3exmid  8807  nnind  8828  peano2uz2  9250  peano5uzti  9251  dfuzi  9253  uzind  9254  uzind3  9256  eluz1  9422  uzind4  9478  supinfneg  9485  infsupneg  9486  eqreznegel  9501  elixx1  9779  elioo2  9803  elfz1  9895  expcl2lemap  10409  expclzaplem  10421  expclzap  10422  expap0i  10429  expge0  10433  expge1  10434  hashennnuni  10630  shftf  10707  reccn2ap  11187  dvdsdivcl  11715  divalgmod  11791  zsupcl  11807  infssuzex  11809  infssuzcldc  11811  bezoutlemsup  11864  dfgcd2  11869  lcmcllem  11915  lcmledvds  11918  lcmgcdlem  11925  1nprm  11962  1idssfct  11963  isprm2  11965  phicl2  12057  hashdvds  12064  oddennn  12072  evenennn  12073  znnen  12078  ennnfonelemg  12083  ennnfonelemom  12088  istopon  12350  epttop  12429  iscld  12442  isnei  12483  neipsm  12493  iscn  12536  iscnp  12538  txdis1cn  12617  ishmeo  12643  ispsmet  12662  ismet  12683  isxmet  12684  elblps  12729  elbl  12730  xmetxpbl  12847  reopnap  12877  divcnap  12894  elcncf  12899  cdivcncfap  12926  cnopnap  12933  ellimc3apf  12968  limccoap  12986  dvlemap  12988  dvidlemap  12999  dvcnp2cntop  13002  dvaddxxbr  13004  dvmulxxbr  13005  dvcoapbr  13010  dvcjbr  13011  dvrecap  13016  dveflem  13026  subctctexmid  13512