Theorem elrab 3593

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) Remove dependency on ax-13 2373. (Revised by Steven Nguyen, 23-Nov-2022.)

Hypothesis

Ref	Expression
elrab.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
elrab	⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem elrab

Step	Hyp	Ref	Expression
1		elex 3418	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V)
2		elex 3418	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 484	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V)
4		eleq1 2821	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		elrab.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
6	4, 5	anbi12d 634	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
7		df-rab 3063	. . 3 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
8	6, 7	elab2g 3580	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
9	1, 3, 8	pm5.21nii 383	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   ∈ wcel 2114  {crab 3058  Vcvv 3400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-rab 3063  df-v 3402

This theorem is referenced by:  elrab3  3594  elrabd  3595  elrab2  3596  ralrab  3598  rexrab  3600  rabsnt  4632  unimax  4844  ssintub  4864  intminss  4872  rabxfrd  5294  ssimaex  6766  weniso  7133  canth  7137  sorpsscmpl  7491  onnminsb  7551  dfom2  7614  ssnlim  7631  elsuppfng  7878  elsuppfn  7879  ressuppssdif  7893  oeeulem  8271  elpmg  8466  fineqvlem  8824  mapfienlem2  8956  supub  9009  suplub  9010  ordtypelem6  9073  ordtypelem7  9074  hartogslem1  9092  hartogs  9094  wemapsolem  9100  card2on  9104  elharval  9111  wdom2d  9130  cantnfs  9215  scottex  9400  tskwe  9465  cardid2  9468  iscard2  9491  cardmin2  9514  acni3  9560  alephsuc2  9593  kmlem1  9663  cofsmo  9782  coftr  9786  fin23lem11  9830  enfin2i  9834  fin1a2lem9  9921  fin1a2lem11  9923  axcc4  9952  axdc3lem2  9964  zorn2lem7  10015  ondomon  10076  alephval2  10085  grutsk  10335  negf1o  11161  infm3  11690  nnind  11747  peano2uz2  12164  peano5uzi  12165  dfuzi  12167  uzind  12168  uzind3  12170  eluz1  12341  uzind4  12401  nnwos  12410  eqreznegel  12429  zmin  12439  elixx1  12843  elioo2  12875  elfz1  12999  flval3  13289  serge0  13529  expge0  13570  expge1  13571  hashbclem  13915  pr2pwpr  13944  elss2prb  13952  hash2sspr  13953  wrdmap  14000  wwlktovfo  14424  shftf  14541  rlimrege0  15039  incexc2  15299  dvdsdivcl  15774  divalglem4  15854  divalgmod  15864  bitsval  15880  bezout  16000  dfgcd2  16003  lcmledvds  16053  lcmgcdlem  16060  lcmfledvds  16086  1nprm  16133  1idssfct  16134  isprm2  16136  hashdvds  16225  phisum  16240  odzval  16241  odzcllem  16242  odzdvds  16245  prmreclem2  16366  prmreclem5  16369  rami  16464  ramub1lem1  16475  ramub1lem2  16476  prmgaplem3  16502  prmgaplem4  16503  prmgaplem5  16504  prmgaplem6  16505  ismre  16977  ismri  17018  isacs  17038  isacs1i  17044  catlid  17070  catrid  17071  ismon  17121  isnat  17335  eldmcoa  17450  fncnvimaeqv  17499  lubeldm  17720  glbeldm  17733  gsumval2  18025  ismhm  18087  issubm  18097  issubmd  18100  mndind  18121  grplinv  18283  issubg  18410  isnsg  18438  cycsubg  18482  isgim  18533  isga  18552  elcntz  18583  elcntzsn  18586  symgfix2  18675  symgsssg  18726  symgfisg  18727  psgnunilem5  18753  odid  18797  odlem2  18798  gexid  18837  gexlem2  18838  gexdvds  18840  isslw  18864  pgpssslw  18870  pj1id  18956  oddvdssubg  19107  pgpfac1lem5  19333  ablfaclem2  19340  isirred  19584  isrim0  19610  issubrg  19667  issdrg  19706  isabv  19722  islss  19838  islmhm  19931  islmim  19966  islbs  19980  psgndiflemB  20429  elocv  20497  isobs  20549  dsmmelbas  20568  frlmelbas  20585  islinds  20638  gsumbagdiaglemOLD  20764  gsumbagdiaglem  20767  psrmulcllem  20779  psrlidm  20795  psrridm  20796  psrass1  20797  psrcom  20801  mplsubglem  20828  mpllsslem  20829  evlsval2  20914  ismhp  20948  ismhp3  20950  mhpmulcl  20956  coe1ae0  21004  coe1mul2  21057  dmatel  21257  scmatel  21269  scmateALT  21276  symgmatr01lem  21417  pmatcoe1fsupp  21465  cpmatel  21475  chpscmat  21606  istopon  21676  fctop  21768  cctop  21770  ppttop  21771  pptbas  21772  epttop  21773  iscld  21791  clscld  21811  isnei  21867  neips  21877  neiptopnei  21896  iscn  21999  iscnp  22001  cmpsublem  22163  conncompconn  22196  2ndc1stc  22215  2ndcdisj  22220  elkgen  22300  xkoccn  22383  txdis1cn  22399  txkgen  22416  xkococnlem  22423  xkococn  22424  xkoinjcn  22451  txconn  22453  elqtop  22461  elmptrab  22591  fbssfi  22601  opnfbas  22606  elfg  22635  cfinfil  22657  csdfil  22658  supfil  22659  filssufilg  22675  uffix  22685  fixufil  22686  uffixfr  22687  elflim2  22728  fclscf  22789  flimfnfcls  22792  alexsubALTlem2  22812  alexsubALTlem4  22814  alexsubALT  22815  ptcmplem2  22817  elutop  22998  isucn  23043  iscfilu  23053  ispsmet  23070  ismet  23089  isxmet  23090  elblps  23153  elbl  23154  restmetu  23336  icccmp  23590  elcncf  23654  ishtpy  23737  isphtpy  23746  om1elbas  23797  iscfil  24030  iscau  24041  iscmet  24049  lmle  24066  rrxfsupp  24167  minveclem3  24194  minveclem4  24197  ovolshftlem1  24274  ovolscalem1  24278  ovolicc2lem3  24284  dyadmax  24363  dyadmbllem  24364  opnmbllem  24366  vitalilem2  24374  vitalilem3  24375  elcpn  24699  ig1pval3  24940  coelem  24988  quotlem  25061  elqaalem1  25080  elqaalem3  25082  aannenlem1  25089  aannenlem2  25090  dmarea  25708  jensen  25739  ftalem4  25826  efnnfsumcl  25853  efchtdvds  25909  sqff1o  25932  fsumdvdsdiaglem  25933  dvdsppwf1o  25936  dvdsflf1o  25937  dvdsflsumcom  25938  musum  25941  muinv  25943  logfac2  25966  dchrelbas  25985  lgsfle1  26055  lgsle1  26061  lgsdirprm  26080  lgsne0  26084  lgsquadlem1  26129  lgsquadlem2  26130  dchrvmasumlem1  26244  logsqvma  26291  pntleml  26360  tgellng  26512  mircgr  26616  mirbtwn  26617  iseqlg  26826  ttgelitv  26842  upgrle  27048  upgrbi  27051  umgredg2  27058  umgrbi  27059  edgupgr  27092  edgumgr  27093  upgredg  27095  numedglnl  27102  edgusgr  27118  usgruspgrb  27139  usgredg2ALT  27148  ushgredgedg  27184  ushgredgedgloop  27186  usgrexmplef  27214  upgrreslem  27259  umgrreslem  27260  upgrres1  27268  nbgrel  27295  nbupgrel  27300  nbumgrvtx  27301  nbusgreledg  27308  nbgrnself  27314  uvtxusgrel  27358  vtxdgoddnumeven  27508  rgrusgrprc  27544  lfgrwlkprop  27642  iswwlks  27787  iswwlksn  27789  wwlksnextsurj  27851  rusgrnumwwlkslem  27920  rusgrnumwwlks  27925  isclwwlk  27934  clwwlknscsh  28012  eleclclwwlkn  28026  clwlknf1oclwwlkn  28034  clwwlkvbij  28063  eupth2lems  28188  konigsberglem4  28205  fusgreg2wsplem  28283  2clwwlkel  28299  extwwlkfabel  28303  clwwlknonclwlknonf1o  28312  dlwwlknondlwlknonf1o  28315  numclwwlk2lem1  28326  numclwlk2lem2f  28327  numclwlk2lem2f1o  28329  grpoidinv2  28463  grpoinv  28473  isssp  28672  islno  28701  isblo  28730  ishmo  28759  ubthlem1  28818  ubthlem2  28819  htthlem  28865  ocel  29229  shsval2i  29335  ococin  29356  chsupsn  29361  eleigvec  29905  cnlnadjlem5  30019  shatomistici  30309  hatomistici  30310  dmrab  30431  nnindf  30721  ismnt  30851  pwrssmgc  30868  tocycf  30974  tocyc01  30975  trsp2cyc  30980  cycpmco2f1  30981  cycpmco2rn  30982  cycpmco2lem2  30984  cycpmco2lem3  30985  cycpmco2lem5  30987  cycpmco2lem6  30988  cycpmco2lem7  30989  cycpmconjv  30999  tocyccntz  31001  cyc3evpm  31007  cycpmgcl  31010  cycpmconjslem2  31012  cyc3conja  31014  nsgmgclem  31181  nsgmgc  31182  nsgqusf1olem2  31184  isprmidl  31198  ismxidl  31219  ssmxidl  31227  isrprm  31250  fedgmullem2  31296  zarclsiin  31406  zart0  31414  rhmpreimacnlem  31419  ordtconnlem1  31459  indf1ofs  31577  sigagenval  31691  ldsysgenld  31711  ldgenpisyslem1  31714  ldgenpisyslem2  31715  ldgenpisys  31717  ddemeas  31787  ismbfm  31802  imambfm  31812  dya2iocuni  31833  oms0  31847  omssubadd  31850  elcarsg  31855  issibf  31883  sitgfval  31891  oddpwdc  31904  eulerpartlemgh  31928  eulerpartlemgs2  31930  dstfrvel  32023  ballotlemfc0  32042  ballotlemfcc  32043  ballotlemiex  32051  ballotlemfrcn0  32079  ballotlemirc  32081  ballotlem7  32085  reprsum  32176  reprsuc  32178  reprpmtf1o  32189  reprdifc  32190  fnrelpredd  32645  connpconn  32781  iscvm  32805  cvmsi  32811  cvmsval  32812  cvmliftmolem2  32828  cvmliftiota  32847  snmlval  32877  satfv1lem  32908  fmlafvel  32931  fmla1  32933  fmlaomn0  32936  satfv0fvfmla0  32959  sategoelfvb  32965  elmpst  33082  riotarab  33259  reurab  33260  sltval2  33515  sltres  33521  conway  33649  scutcut  33651  scutbday  33654  scutun12  33660  scutbdaybnd2  33666  scutbdaylt  33668  bday1s  33681  lineelsb2  34106  linerflx1  34107  fwddifval  34120  fwddifnval  34121  rankeq1o  34129  finminlem  34163  fneint  34193  fnessref  34202  topmeet  34209  topjoin  34210  neifg  34216  relowlssretop  35190  fin2solem  35419  fin2so  35420  poimirlem4  35437  poimirlem25  35458  poimirlem26  35459  poimirlem27  35460  poimirlem31  35464  poimirlem32  35465  opnmbllem0  35469  mblfinlem2  35471  itg2gt0cn  35488  indexa  35547  nninfnub  35565  istotbnd  35583  sstotbnd2  35588  isbnd  35594  isrngohom  35779  isrngoiso  35792  isidl  35828  ispridl  35848  ismaxidl  35854  prnc  35881  isfldidl  35882  islshp  36649  lssats  36682  islfl  36730  isat  36956  atlatmstc  36989  islln  37176  islpln  37200  islvol  37243  linepsubN  37422  elpmap  37428  pmapsub  37438  elpadd  37469  paddvaln0N  37471  islhp  37666  isldil  37780  isltrn  37789  isdilN  37824  istrnN  37827  diaval  38702  diaelval  38703  diaeldm  38706  diaelrnN  38715  cdlemm10N  38788  docaclN  38794  dibglbN  38836  dicval  38846  dicfnN  38853  dicvalrelN  38855  dihglblem2aN  38963  dihglblem2N  38964  dihglblem3N  38965  dih1dimatlem  38999  dihglb2  39012  dochvalr  39027  doch2val2  39034  dochocss  39036  islpolN  39153  mapd0  39335  sticksstones3  39743  fsuppssindlem2  39901  infdesc  40093  isnacs  40139  elmzpcl  40161  mzpindd  40181  rencldnfilem  40255  irrapxlem6  40262  pellexlem3  40266  pellexlem5  40268  elpell1qr  40282  elpell14qr  40284  elpell1234qr  40286  pellfundre  40316  pellfundge  40317  pellfundlb  40319  pellfundglb  40320  rmspecnonsq  40342  jm2.22  40430  jm2.23  40431  rpnnen3lem  40466  fnwe2lem2  40489  elmnc  40574  dgraalem  40583  dgraaub  40586  mpaalem  40590  rgspnmin  40609  sqrtcvallem1  40825  rfovcnvf1od  41199  scottelrankd  41448  nzss  41514  iccshift  42637  iooshift  42641  limcperiod  42752  sumnnodd  42754  ioodvbdlimc1lem1  43055  dvnprodlem1  43070  dvnprodlem3  43072  itgperiod  43105  stoweidlem14  43138  stoweidlem15  43139  stoweidlem16  43140  stoweidlem31  43155  stoweidlem36  43160  stoweidlem46  43170  stoweidlem48  43172  fourierdlem2  43233  fourierdlem3  43234  fourierdlem20  43251  fourierdlem25  43256  fourierdlem37  43268  fourierdlem42  43273  fourierdlem48  43278  fourierdlem51  43281  fourierdlem63  43293  fourierdlem64  43294  fourierdlem65  43295  fourierdlem79  43309  fourierdlem81  43311  elaa2lem  43357  etransclem24  43382  etransclem26  43384  etransclem28  43386  etransclem35  43393  etransclem48  43406  salgenval  43445  salgenn0  43453  salgencl  43454  sssalgen  43457  salgenss  43458  salgenuni  43459  issalgend  43460  salgencntex  43465  subsaliuncllem  43479  sge0fodjrnlem  43537  meadjiunlem  43586  caragenel  43616  ovnlecvr  43679  ovnpnfelsup  43680  ovncvrrp  43685  ovnsubaddlem1  43691  hoidmv1lelem1  43712  hoidmv1lelem2  43713  hoidmv1lelem3  43714  hoidmvlelem1  43716  hoidmvlelem2  43717  hoidmvlelem4  43719  ovnhoilem1  43722  ovnlecvr2  43731  ovncvr2  43732  issmflem  43843  smflimlem2  43887  smflimlem3  43888  smflimsuplem2  43934  elsetpreimafvrab  44428  iccpart  44450  sprel  44518  prelspr  44520  sprsymrelfolem2  44527  sprsymrelf  44529  prpair  44535  paireqne  44545  prprelb  44550  prprelprb  44551  dfodd2  44670  dfeven5  44700  dfodd7  44701  fpprel  44762  1hegrlfgr  44876  ismgmhm  44919  issubmgm  44925  rabsubmgmd  44927  mgmhmeql  44939  assintop  44985  isassintop  44986  assintopcllaw  44988  isrnghm  45032  isrngisom  45036  0even  45071  2even  45073  2zrngamgm  45079  dmatALTbasel  45325  lcoval  45335  elbigo  45479  elrrx2linest2  45673  itsclc0  45699  itsclc0b  45700  itscnhlinecirc02p  45713  secval  45950  cscval  45951  cotval  45952