Theorem elrab 2982

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  {crab 2532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rab 2537  df-v 2823

This theorem is used by:  elrab3  2983  elrabd  2984  elrab2  2985  ralrab  2987  rexrab  2989  rabsnt  3786  unimax  3969  ssintub  3988  intminss  3995  exmidexmid  4335  exmidsssnc  4342  rabxfrd  4617  ordtri2or2exmidlem  4675  onsucelsucexmidlem1  4677  sefvex  5719  ssimaex  5767  acexmidlem2  6085  elsuppfng  6486  elsuppfn  6487  elpmg  6942  ssfilem  7181  ssfilemd  7183  diffitest  7195  inffiexmid  7217  2omap  7324  supubti  7345  suplubti  7346  ctssexmid  7496  sspw1or2  7550  exmidonfinlem  7551  finacn  7566  cc4f  7641  cc4n  7643  acnccim  7644  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemdisj  8093  suplocexprlemub  8096  nnindnn  8266  negf1o  8716  apsscn  8983  sup3exmid  9295  nnind  9329  peano2uz2  9764  peano5uzti  9765  dfuzi  9767  uzind  9768  uzind3  9770  eluz1  9941  uzind4  10004  supinfneg  10011  infsupneg  10012  eqreznegel  10030  elixx1  10316  elioo2  10340  elfz1  10433  zsupcl  10681  infssuzex  10683  infssuzcldc  10685  expcl2lemap  11009  expclzaplem  11021  expclzap  11022  expap0i  11029  expge0  11033  expge1  11034  hashennnuni  11240  hashfibclem  11304  wrdmap  11358  shftf  11617  reccn2ap  12104  dvdsdivcl  12642  divalgmod  12719  bitsval  12735  bitsfzolem  12746  bezoutlemsup  12811  dfgcd2  12816  uzwodc  12839  nnwosdc  12841  nninfctlemfo  12842  lcmgcdlem  12880  1nprm  12917  1idssfct  12918  isprm2  12920  phicl2  13021  hashdvds  13028  dvdsfi  13046  phisum  13048  odzval  13049  odzcllem  13050  odzdvds  13053  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemiex  13302  ballotfilemimin  13307  ballotfilemfrcn0  13331  ballotfilemirc  13333  ballotfilem7  13337  oddennn  13341  evenennn  13342  znnen  13347  ennnfonelemg  13352  ennnfonelemom  13357  ismhm  13827  issubm  13838  issubmd  13840  grplinv  13914  issubg  14035  isnsg  14064  elcntz  14154  elcntzsn  14157  isrim0  14577  issubrng  14616  issubrg  14638  ringunitsap0  14703  drnguiap  14718  islssm  14803  islssmg  14804  cnfldui  15033  gsumbagdiaglem  15175  rhmpsrfilem2  15185  psrlidmfi  15199  psrridmfi  15200  psrass1fi  15201  mplelbascoe  15208  istopon  15239  epttop  15316  iscld  15329  isnei  15370  neipsm  15380  iscn  15423  iscnp  15425  txdis1cn  15504  ishmeo  15530  ispsmet  15549  ismet  15570  isxmet  15571  elblps  15616  elbl  15617  xmetxpbl  15734  reopnap  15772  divcnap  15791  elcncf  15799  cdivcncfap  15830  cnopnap  15837  divcncfap  15840  maxcncf  15841  mincncf  15842  ellimc3apf  15886  limccoap  15904  dvlemap  15906  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvcnp2cntop  15925  dvaddxxbr  15927  dvmulxxbr  15928  dvcoapbr  15933  dvcjbr  15934  dvrecap  15939  dveflem  15952  pellexlem3  16231  efnnfsumcl  16239  prmdvdsfi  16243  efchtqdvds  16265  dvdsppwf1o  16283  ppiqub  16293  lgsfle1  16333  lgsle1  16339  lgsdirprm  16358  lgsne0  16362  lgsquadlem1  16401  lgsquadlem2  16402  uhgrm  16524  upgrm  16546  upgr1or2  16547  umgredg2en  16555  umgrbien  16556  uhgredgm  16582  edgupgren  16587  edgumgren  16588  edgusgren  16609  usgruspgrben  16632  ushgredgedg  16672  ushgredgedgloop  16674  isclwwlk  16840  isclwwlkng  16852  clwwlknon  16875  eupth2lemsfi  16924  konigsberglem1  16934  konigsberglem4  16937  pw1map  17230  subctctexmid  17235  wexmiddiffilem  17248