Theorem elrab 2916

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rab 2481  df-v 2762

This theorem is referenced by:  elrab3  2917  elrabd  2918  elrab2  2919  ralrab  2921  rexrab  2923  rabsnt  3693  unimax  3869  ssintub  3888  intminss  3895  exmidexmid  4225  exmidsssnc  4232  rabxfrd  4500  ordtri2or2exmidlem  4558  onsucelsucexmidlem1  4560  sefvex  5575  ssimaex  5618  acexmidlem2  5915  elpmg  6718  ssfilem  6931  diffitest  6943  inffiexmid  6962  supubti  7058  suplubti  7059  ctssexmid  7209  exmidonfinlem  7253  cc4f  7329  cc4n  7331  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  suplocexprlemmu  7778  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemub  7783  nnindnn  7953  negf1o  8401  apsscn  8666  sup3exmid  8976  nnind  8998  peano2uz2  9424  peano5uzti  9425  dfuzi  9427  uzind  9428  uzind3  9430  eluz1  9596  uzind4  9653  supinfneg  9660  infsupneg  9661  eqreznegel  9679  elixx1  9963  elioo2  9987  elfz1  10079  expcl2lemap  10622  expclzaplem  10634  expclzap  10635  expap0i  10642  expge0  10646  expge1  10647  hashennnuni  10850  wrdmap  10945  shftf  10974  reccn2ap  11456  dvdsdivcl  11992  divalgmod  12068  zsupcl  12084  infssuzex  12086  infssuzcldc  12088  bezoutlemsup  12146  dfgcd2  12151  uzwodc  12174  nnwosdc  12176  nninfctlemfo  12177  lcmgcdlem  12215  1nprm  12252  1idssfct  12253  isprm2  12255  phicl2  12352  hashdvds  12359  phisum  12378  odzval  12379  odzcllem  12380  odzdvds  12383  oddennn  12549  evenennn  12550  znnen  12555  ennnfonelemg  12560  ennnfonelemom  12565  ismhm  13033  issubm  13044  issubmd  13046  grplinv  13122  issubg  13243  isnsg  13272  isrim0  13657  issubrng  13695  issubrg  13717  islssm  13853  islssmg  13854  cnfldui  14077  istopon  14181  epttop  14258  iscld  14271  isnei  14312  neipsm  14322  iscn  14365  iscnp  14367  txdis1cn  14446  ishmeo  14472  ispsmet  14491  ismet  14512  isxmet  14513  elblps  14558  elbl  14559  xmetxpbl  14676  reopnap  14706  divcnap  14723  elcncf  14728  cdivcncfap  14758  cnopnap  14765  divcncfap  14768  maxcncf  14769  mincncf  14770  ellimc3apf  14814  limccoap  14832  dvlemap  14834  dvidlemap  14845  dvcnp2cntop  14848  dvaddxxbr  14850  dvmulxxbr  14851  dvcoapbr  14856  dvcjbr  14857  dvrecap  14862  dveflem  14872  lgsfle1  15125  lgsle1  15131  lgsdirprm  15150  lgsne0  15154  lgsquadlem1  15191  subctctexmid  15491