Theorem elrab 2920

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

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364   ∈ wcel 2167  {crab 2479

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rab 2484  df-v 2765

This theorem is referenced by:  elrab3  2921  elrabd  2922  elrab2  2923  ralrab  2925  rexrab  2927  rabsnt  3698  unimax  3874  ssintub  3893  intminss  3900  exmidexmid  4230  exmidsssnc  4237  rabxfrd  4505  ordtri2or2exmidlem  4563  onsucelsucexmidlem1  4565  sefvex  5582  ssimaex  5625  acexmidlem2  5922  elpmg  6732  ssfilem  6945  diffitest  6957  inffiexmid  6976  supubti  7074  suplubti  7075  ctssexmid  7225  exmidonfinlem  7272  finacn  7287  cc4f  7352  cc4n  7354  acnccim  7355  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  suplocexprlemmu  7802  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemub  7807  nnindnn  7977  negf1o  8425  apsscn  8691  sup3exmid  9001  nnind  9023  peano2uz2  9450  peano5uzti  9451  dfuzi  9453  uzind  9454  uzind3  9456  eluz1  9622  uzind4  9679  supinfneg  9686  infsupneg  9687  eqreznegel  9705  elixx1  9989  elioo2  10013  elfz1  10105  zsupcl  10338  infssuzex  10340  infssuzcldc  10342  expcl2lemap  10660  expclzaplem  10672  expclzap  10673  expap0i  10680  expge0  10684  expge1  10685  hashennnuni  10888  wrdmap  10983  shftf  11012  reccn2ap  11495  dvdsdivcl  12032  divalgmod  12109  bitsval  12125  bitsfzolem  12136  bezoutlemsup  12201  dfgcd2  12206  uzwodc  12229  nnwosdc  12231  nninfctlemfo  12232  lcmgcdlem  12270  1nprm  12307  1idssfct  12308  isprm2  12310  phicl2  12407  hashdvds  12414  dvdsfi  12432  phisum  12434  odzval  12435  odzcllem  12436  odzdvds  12439  oddennn  12634  evenennn  12635  znnen  12640  ennnfonelemg  12645  ennnfonelemom  12650  ismhm  13163  issubm  13174  issubmd  13176  grplinv  13252  issubg  13379  isnsg  13408  isrim0  13793  issubrng  13831  issubrg  13853  islssm  13989  islssmg  13990  cnfldui  14221  istopon  14333  epttop  14410  iscld  14423  isnei  14464  neipsm  14474  iscn  14517  iscnp  14519  txdis1cn  14598  ishmeo  14624  ispsmet  14643  ismet  14664  isxmet  14665  elblps  14710  elbl  14711  xmetxpbl  14828  reopnap  14866  divcnap  14885  elcncf  14893  cdivcncfap  14924  cnopnap  14931  divcncfap  14934  maxcncf  14935  mincncf  14936  ellimc3apf  14980  limccoap  14998  dvlemap  15000  dvidlemap  15011  dvidrelem  15012  dvidsslem  15013  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvrecap  15033  dveflem  15046  dvdsppwf1o  15309  lgsfle1  15334  lgsle1  15340  lgsdirprm  15359  lgsne0  15363  lgsquadlem1  15402  lgsquadlem2  15403  2omap  15726  subctctexmid  15731