Theorem elrab 2893

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353   ∈ wcel 2148  {crab 2459

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rab 2464  df-v 2739

This theorem is referenced by:  elrab3  2894  elrabd  2895  elrab2  2896  ralrab  2898  rexrab  2900  rabsnt  3667  unimax  3843  ssintub  3862  intminss  3869  exmidexmid  4196  exmidsssnc  4203  rabxfrd  4469  ordtri2or2exmidlem  4525  onsucelsucexmidlem1  4527  sefvex  5536  ssimaex  5577  acexmidlem2  5871  elpmg  6663  ssfilem  6874  diffitest  6886  inffiexmid  6905  supubti  6997  suplubti  6998  ctssexmid  7147  exmidonfinlem  7191  cc4f  7267  cc4n  7269  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  suplocexprlemmu  7716  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemub  7721  nnindnn  7891  negf1o  8338  apsscn  8603  sup3exmid  8913  nnind  8934  peano2uz2  9359  peano5uzti  9360  dfuzi  9362  uzind  9363  uzind3  9365  eluz1  9531  uzind4  9587  supinfneg  9594  infsupneg  9595  eqreznegel  9613  elixx1  9896  elioo2  9920  elfz1  10012  expcl2lemap  10531  expclzaplem  10543  expclzap  10544  expap0i  10551  expge0  10555  expge1  10556  hashennnuni  10758  shftf  10838  reccn2ap  11320  dvdsdivcl  11855  divalgmod  11931  zsupcl  11947  infssuzex  11949  infssuzcldc  11951  bezoutlemsup  12009  dfgcd2  12014  uzwodc  12037  nnwosdc  12039  lcmcllem  12066  lcmledvds  12069  lcmgcdlem  12076  1nprm  12113  1idssfct  12114  isprm2  12116  phicl2  12213  hashdvds  12220  phisum  12239  odzval  12240  odzcllem  12241  odzdvds  12244  oddennn  12392  evenennn  12393  znnen  12398  ennnfonelemg  12403  ennnfonelemom  12408  ismhm  12852  issubm  12862  issubmd  12864  grplinv  12921  issubg  13031  isnsg  13060  issubrg  13340  istopon  13483  epttop  13560  iscld  13573  isnei  13614  neipsm  13624  iscn  13667  iscnp  13669  txdis1cn  13748  ishmeo  13774  ispsmet  13793  ismet  13814  isxmet  13815  elblps  13860  elbl  13861  xmetxpbl  13978  reopnap  14008  divcnap  14025  elcncf  14030  cdivcncfap  14057  cnopnap  14064  ellimc3apf  14099  limccoap  14117  dvlemap  14119  dvidlemap  14130  dvcnp2cntop  14133  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  dvcjbr  14142  dvrecap  14147  dveflem  14157  lgsfle1  14380  lgsle1  14386  lgsdirprm  14405  lgsne0  14409  subctctexmid  14720