Theorem elrab 3650

Description: Membership in a restricted class abstraction, using implicit substitution. (Contributed by NM, 21-May-1999.) Remove dependency on ax-13 2370. (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 3459	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V)
2		elex 3459	. . 3 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ V)
3	2	adantr 480	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ 𝜓) → 𝐴 ∈ V)
4		eleq1 2816	. . . 4 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
5		elrab.1	. . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓))
6	4, 5	anbi12d 632	. . 3 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝜑) ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
7		df-rab 3397	. . 3 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
8	6, 7	elab2g 3638	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
9	1, 3, 8	pm5.21nii 378	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {crab 3396  Vcvv 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440

This theorem is referenced by:  elrab3  3651  elrabd  3652  elrab2  3653  ralrab  3656  rexrab  3658  reurab  3663  rabsnt  4685  unimax  4897  ssintub  4919  intminss  4927  rabxfrd  5359  ssimaex  6912  weniso  7295  canth  7307  riotarab  7352  sorpsscmpl  7674  onnminsb  7739  dfom2  7808  ssnlim  7826  elsuppfng  8109  elsuppfn  8110  ressuppssdif  8125  oeeulem  8526  cofonr  8599  elpmg  8777  fineqvlem  9167  mapfienlem2  9315  supub  9368  suplub  9369  ordtypelem6  9434  ordtypelem7  9435  hartogslem1  9453  hartogs  9455  wemapsolem  9461  card2on  9465  elharval  9472  wdom2d  9491  cantnfs  9581  scottex  9800  tskwe  9865  cardid2  9868  iscard2  9891  cardmin2  9914  acni3  9960  alephsuc2  9993  kmlem1  10064  cofsmo  10182  coftr  10186  fin23lem11  10230  enfin2i  10234  fin1a2lem9  10321  fin1a2lem11  10323  axcc4  10352  axdc3lem2  10364  zorn2lem7  10415  ondomon  10476  alephval2  10485  grutsk  10735  negf1o  11568  infm3  12102  nnind  12164  peano2uz2  12582  peano5uzi  12583  dfuzi  12585  uzind  12586  uzind3  12588  eluz1  12757  uzind4  12825  nnwos  12834  eqreznegel  12853  zmin  12863  elixx1  13275  elioo2  13307  elfz1  13433  flval3  13737  serge0  13981  expge0  14023  expge1  14024  hashbclem  14377  pr2pwpr  14404  elss2prb  14413  hash2sspr  14414  wrdmap  14471  wwlktovfo  14883  shftf  15004  rlimrege0  15504  incexc2  15763  dvdsdivcl  16245  divalglem4  16325  divalgmod  16335  bitsval  16353  bezout  16472  dfgcd2  16475  lcmledvds  16528  lcmgcdlem  16535  lcmfledvds  16561  1nprm  16608  1idssfct  16609  isprm2  16611  hashdvds  16704  phisum  16720  odzval  16721  odzcllem  16722  odzdvds  16725  prmreclem2  16847  prmreclem5  16850  rami  16945  ramub1lem1  16956  ramub1lem2  16957  prmgaplem3  16983  prmgaplem4  16984  prmgaplem5  16985  prmgaplem6  16986  ismre  17510  ismri  17555  isacs  17575  isacs1i  17581  catlid  17607  catrid  17608  ismon  17658  isnat  17875  eldmcoa  17990  fncnvimaeqv  18044  lubeldm  18275  glbeldm  18288  gsumval2  18578  ismgmhm  18588  issubmgm  18594  rabsubmgmd  18596  mgmhmeql  18608  ismhm  18677  issubm  18695  issubmd  18698  mndind  18720  grplinv  18886  issubg  19023  isnsg  19052  cycsubg  19105  isgim  19159  isga  19188  elcntz  19219  elcntzsn  19222  symgfix2  19313  symgsssg  19364  symgfisg  19365  psgnunilem5  19391  odid  19435  odlem2  19436  gexid  19478  gexlem2  19479  gexdvds  19481  isslw  19505  pgpssslw  19511  pj1id  19596  oddvdssubg  19752  pgpfac1lem5  19978  ablfaclem2  19985  isirred  20322  isrnghm  20344  isrngim  20348  isrim0OLD  20384  isrim0  20386  issubrng  20450  issubrg  20474  rgspnmin  20518  issdrg  20691  isabv  20714  islss  20855  islmhm  20949  islmim  20984  islbs  20998  psgndiflemB  21525  elocv  21593  isobs  21645  dsmmelbas  21664  frlmelbas  21681  islinds  21734  gsumbagdiaglem  21855  rhmpsrlem2  21866  psrlidm  21887  psrridm  21888  psrass1  21889  psrcom  21893  mplsubglem  21924  mpllsslem  21925  evlsval2  22010  ismhp  22043  ismhp3  22045  mhpmulcl  22052  psdmul  22069  coe1ae0  22117  coe1mul2  22171  dmatel  22396  scmatel  22408  scmateALT  22415  symgmatr01lem  22556  pmatcoe1fsupp  22604  cpmatel  22614  chpscmat  22745  istopon  22815  fctop  22907  cctop  22909  ppttop  22910  pptbas  22911  epttop  22912  iscld  22930  clscld  22950  isnei  23006  neips  23016  neiptopnei  23035  iscn  23138  iscnp  23140  cmpsublem  23302  conncompconn  23335  2ndc1stc  23354  2ndcdisj  23359  elkgen  23439  xkoccn  23522  txdis1cn  23538  txkgen  23555  xkococnlem  23562  xkococn  23563  xkoinjcn  23590  txconn  23592  elqtop  23600  elmptrab  23730  fbssfi  23740  opnfbas  23745  elfg  23774  cfinfil  23796  csdfil  23797  supfil  23798  filssufilg  23814  uffix  23824  fixufil  23825  uffixfr  23826  elflim2  23867  fclscf  23928  flimfnfcls  23931  alexsubALTlem2  23951  alexsubALTlem4  23953  alexsubALT  23954  ptcmplem2  23956  elutop  24137  isucn  24181  iscfilu  24191  ispsmet  24208  ismet  24227  isxmet  24228  elblps  24291  elbl  24292  restmetu  24474  icccmp  24730  elcncf  24798  ishtpy  24887  isphtpy  24896  om1elbas  24948  iscfil  25181  iscau  25192  iscmet  25200  lmle  25217  rrxfsupp  25318  minveclem3  25345  minveclem4  25348  ovolshftlem1  25426  ovolscalem1  25430  ovolicc2lem3  25436  dyadmax  25515  dyadmbllem  25516  opnmbllem  25518  vitalilem2  25526  vitalilem3  25527  elcpn  25852  ig1pval3  26099  coelem  26147  quotlem  26224  elqaalem1  26243  elqaalem3  26245  aannenlem1  26252  aannenlem2  26253  dmarea  26883  jensen  26915  ftalem4  27002  efnnfsumcl  27029  efchtdvds  27085  sqff1o  27108  fsumdvdsdiaglem  27109  dvdsppwf1o  27112  dvdsflf1o  27113  dvdsflsumcom  27114  musum  27117  muinv  27119  logfac2  27144  dchrelbas  27163  lgsfle1  27233  lgsle1  27239  lgsdirprm  27258  lgsne0  27262  lgsquadlem1  27307  lgsquadlem2  27308  dchrvmasumlem1  27422  logsqvma  27469  pntleml  27538  sltval2  27584  sltres  27590  conway  27728  scutcut  27730  scutbday  27733  scutun12  27739  scutbdaybnd2  27745  scutbdaylt  27747  bday1s  27763  cutlt  27863  precsexlem8  28139  precsexlem9  28140  precsexlem11  28142  onscutlt  28188  noseqinds  28210  peano5uzs  28315  uzsind  28316  tgellng  28516  mircgr  28620  mirbtwn  28621  iseqlg  28830  ttgelitv  28846  upgrle  29053  upgrbi  29056  umgredg2  29063  umgrbi  29064  edgupgr  29097  edgumgr  29098  upgredg  29100  numedglnl  29107  edgusgr  29123  usgruspgrb  29146  usgredg2ALT  29156  ushgredgedg  29192  ushgredgedgloop  29194  usgrexmplef  29222  upgrreslem  29267  umgrreslem  29268  upgrres1  29276  nbgrel  29303  nbupgrel  29308  nbumgrvtx  29309  nbusgreledg  29316  nbgrnself  29322  uvtxusgrel  29366  vtxdgoddnumeven  29517  rgrusgrprc  29553  lfgrwlkprop  29649  iswwlks  29799  iswwlksn  29801  wwlksnextsurj  29863  rusgrnumwwlkslem  29932  rusgrnumwwlks  29937  isclwwlk  29946  clwwlknscsh  30024  eleclclwwlkn  30038  clwlknf1oclwwlkn  30046  clwwlkvbij  30075  eupth2lems  30200  konigsberglem4  30217  fusgreg2wsplem  30295  2clwwlkel  30311  extwwlkfabel  30315  clwwlknonclwlknonf1o  30324  dlwwlknondlwlknonf1o  30327  numclwwlk2lem1  30338  numclwlk2lem2f  30339  numclwlk2lem2f1o  30341  grpoidinv2  30477  grpoinv  30487  isssp  30686  islno  30715  isblo  30744  ishmo  30773  ubthlem1  30832  ubthlem2  30833  htthlem  30879  ocel  31243  shsval2i  31349  ococin  31370  chsupsn  31375  eleigvec  31919  cnlnadjlem5  32033  shatomistici  32323  hatomistici  32324  dmrab  32459  nnindf  32777  indf1ofs  32822  ismnt  32938  pwrssmgc  32955  tocycf  33072  tocyc01  33073  trsp2cyc  33078  cycpmco2f1  33079  cycpmco2rn  33080  cycpmco2lem2  33082  cycpmco2lem3  33083  cycpmco2lem5  33085  cycpmco2lem6  33086  cycpmco2lem7  33087  cycpmconjv  33097  tocyccntz  33099  cyc3evpm  33105  cycpmgcl  33108  cycpmconjslem2  33110  cyc3conja  33112  isfxp  33123  fxpgaeq  33124  elrgspnsubrun  33202  fldgensdrg  33266  nsgmgclem  33361  nsgmgc  33362  nsgqusf1olem2  33364  isprmidl  33388  ismxidl  33412  ssmxidl  33424  isrprm  33467  1arithufdlem3  33496  1arithufdlem4  33497  1arithufd  33498  fedgmullem2  33605  ply1annnr  33672  minplyann  33678  minplyirred  33680  constrsuc  33707  zarclsiin  33840  zart0  33848  rhmpreimacnlem  33853  ordtconnlem1  33893  sigagenval  34109  ldsysgenld  34129  ldgenpisyslem1  34132  ldgenpisyslem2  34133  ldgenpisys  34135  ddemeas  34205  ismbfm  34220  imambfm  34232  dya2iocuni  34253  oms0  34267  omssubadd  34270  elcarsg  34275  issibf  34303  sitgfval  34311  oddpwdc  34324  eulerpartlemgh  34348  eulerpartlemgs2  34350  dstfrvel  34444  ballotlemfc0  34463  ballotlemfcc  34464  ballotlemiex  34472  ballotlemfrcn0  34500  ballotlemirc  34502  ballotlem7  34506  reprsum  34583  reprsuc  34585  reprpmtf1o  34596  reprdifc  34597  fnrelpredd  35058  connpconn  35210  iscvm  35234  cvmsi  35240  cvmsval  35241  cvmliftmolem2  35257  cvmliftiota  35276  snmlval  35306  satfv1lem  35337  fmlafvel  35360  fmla1  35362  fmlaomn0  35365  satfv0fvfmla0  35388  sategoelfvb  35394  elmpst  35511  lineelsb2  36124  linerflx1  36125  fwddifval  36138  fwddifnval  36139  rankeq1o  36147  finminlem  36294  fneint  36324  fnessref  36333  topmeet  36340  topjoin  36341  neifg  36347  weiunlem2  36439  weiunfrlem  36440  weiunse  36444  relowlssretop  37339  fin2solem  37588  fin2so  37589  poimirlem4  37606  poimirlem25  37627  poimirlem26  37628  poimirlem27  37629  poimirlem31  37633  poimirlem32  37634  opnmbllem0  37638  mblfinlem2  37640  itg2gt0cn  37657  indexa  37715  nninfnub  37733  istotbnd  37751  sstotbnd2  37756  isbnd  37762  isrngohom  37947  isrngoiso  37960  isidl  37996  ispridl  38016  ismaxidl  38022  prnc  38049  isfldidl  38050  islshp  38960  lssats  38993  islfl  39041  isat  39267  atlatmstc  39300  islln  39488  islpln  39512  islvol  39555  linepsubN  39734  elpmap  39740  pmapsub  39750  elpadd  39781  paddvaln0N  39783  islhp  39978  isldil  40092  isltrn  40101  isdilN  40136  istrnN  40139  diaval  41014  diaelval  41015  diaeldm  41018  diaelrnN  41027  cdlemm10N  41100  docaclN  41106  dibglbN  41148  dicval  41158  dicfnN  41165  dicvalrelN  41167  dihglblem2aN  41275  dihglblem2N  41276  dihglblem3N  41277  dih1dimatlem  41311  dihglb2  41324  dochvalr  41339  doch2val2  41346  dochocss  41348  islpolN  41465  mapd0  41647  aks4d1p4  42055  aks4d1p7  42059  isprimroot  42069  linvh  42072  primrootsunit1  42073  primrootscoprmpow  42075  primrootscoprbij  42078  sticksstones3  42124  aks6d1c6lem3  42148  grpods  42170  unitscyglem2  42172  unitscyglem4  42174  unitscyglem5  42175  supinf  42218  fsuppssindlem2  42568  infdesc  42619  isnacs  42680  elmzpcl  42702  mzpindd  42722  rencldnfilem  42796  irrapxlem6  42803  pellexlem3  42807  pellexlem5  42809  elpell1qr  42823  elpell14qr  42825  elpell1234qr  42827  pellfundre  42857  pellfundge  42858  pellfundlb  42860  pellfundglb  42861  rmspecnonsq  42883  jm2.22  42971  jm2.23  42972  rpnnen3lem  43007  fnwe2lem2  43027  elmnc  43112  dgraalem  43121  dgraaub  43124  mpaalem  43128  onsucelab  43239  limnsuc  43241  sqrtcvallem1  43607  rfovcnvf1od  43980  scottelrankd  44223  nzss  44293  iccshift  45503  iooshift  45507  limcperiod  45613  sumnnodd  45615  ioodvbdlimc1lem1  45916  dvnprodlem1  45931  dvnprodlem3  45933  itgperiod  45966  stoweidlem14  45999  stoweidlem15  46000  stoweidlem16  46001  stoweidlem31  46016  stoweidlem36  46021  stoweidlem46  46031  stoweidlem48  46033  fourierdlem2  46094  fourierdlem3  46095  fourierdlem20  46112  fourierdlem25  46117  fourierdlem37  46129  fourierdlem42  46134  fourierdlem48  46139  fourierdlem51  46142  fourierdlem63  46154  fourierdlem64  46155  fourierdlem65  46156  fourierdlem79  46170  fourierdlem81  46172  elaa2lem  46218  etransclem24  46243  etransclem26  46245  etransclem28  46247  etransclem35  46254  etransclem48  46267  salgenval  46306  salgenn0  46316  salgencl  46317  sssalgen  46320  salgenss  46321  salgenuni  46322  issalgend  46323  salgencntex  46328  subsaliuncllem  46342  sge0fodjrnlem  46401  meadjiunlem  46450  caragenel  46480  ovnlecvr  46543  ovnpnfelsup  46544  ovncvrrp  46549  ovnsubaddlem1  46555  hoidmv1lelem1  46576  hoidmv1lelem2  46577  hoidmv1lelem3  46578  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem4  46583  ovnhoilem1  46586  ovnlecvr2  46595  ovncvr2  46596  issmflem  46712  smflimlem2  46757  smflimlem3  46758  smflimsuplem2  46806  elsetpreimafvrab  47382  iccpart  47404  sprel  47472  prelspr  47474  sprsymrelfolem2  47481  sprsymrelf  47483  prpair  47489  paireqne  47499  prprelb  47504  prprelprb  47505  dfodd2  47624  dfeven5  47654  dfodd7  47655  fpprel  47716  clnbgrel  47816  clnbupgrel  47822  sclnbgrel  47835  vopnbgrel  47842  dfclnbgr6  47844  dfnbgr6  47845  isubgredg  47854  uhgrimisgrgric  47919  grtriprop  47929  isgrtri  47931  stgredgel  47945  stgrusgra  47947  uspgrlimlem3  47978  uspgrlim  47980  grlimgredgex  47988  grlimgrtrilem2  47990  gpgiedgdmel  48037  gpgedgel  48038  gpgnbgrvtx0  48062  gpgnbgrvtx1  48063  gpgprismgr4cycllem10  48092  1hegrlfgr  48120  assintop  48197  isassintop  48198  assintopcllaw  48200  0even  48225  2even  48227  2zrngamgm  48233  dmatALTbasel  48391  lcoval  48401  elbigo  48540  elrrx2linest2  48734  itsclc0  48760  itsclc0b  48761  itscnhlinecirc02p  48774  unilbss  48806  secval  49736  cscval  49737  cotval  49738