Theorem elrab 3648

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3401  Vcvv 3442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444

This theorem is referenced by:  elrab3  3649  elrabd  3650  elrab2  3651  ralrab  3654  rexrab  3656  reurab  3661  rabsnt  4690  unimax  4902  ssintub  4923  intminss  4931  rabxfrd  5364  ssimaex  6927  weniso  7310  canth  7322  riotarab  7367  sorpsscmpl  7689  onnminsb  7754  dfom2  7820  ssnlim  7838  elsuppfng  8121  elsuppfn  8122  ressuppssdif  8137  oeeulem  8539  cofonr  8612  elpmg  8792  fineqvlem  9178  mapfienlem2  9321  supub  9374  suplub  9375  ordtypelem6  9440  ordtypelem7  9441  hartogslem1  9459  hartogs  9461  wemapsolem  9467  card2on  9471  elharval  9478  wdom2d  9497  cantnfs  9587  scottex  9809  tskwe  9874  cardid2  9877  iscard2  9900  cardmin2  9923  acni3  9969  alephsuc2  10002  kmlem1  10073  cofsmo  10191  coftr  10195  fin23lem11  10239  enfin2i  10243  fin1a2lem9  10330  fin1a2lem11  10332  axcc4  10361  axdc3lem2  10373  zorn2lem7  10424  ondomon  10485  alephval2  10495  grutsk  10745  negf1o  11579  infm3  12113  nnind  12175  peano2uz2  12592  peano5uzi  12593  dfuzi  12595  uzind  12596  uzind3  12598  eluz1  12767  uzind4  12831  nnwos  12840  eqreznegel  12859  zmin  12869  elixx1  13282  elioo2  13314  elfz1  13440  flval3  13747  serge0  13991  expge0  14033  expge1  14034  hashbclem  14387  pr2pwpr  14414  elss2prb  14423  hash2sspr  14424  wrdmap  14481  wwlktovfo  14893  shftf  15014  rlimrege0  15514  incexc2  15773  dvdsdivcl  16255  divalglem4  16335  divalgmod  16345  bitsval  16363  bezout  16482  dfgcd2  16485  lcmledvds  16538  lcmgcdlem  16545  lcmfledvds  16571  1nprm  16618  1idssfct  16619  isprm2  16621  hashdvds  16714  phisum  16730  odzval  16731  odzcllem  16732  odzdvds  16735  prmreclem2  16857  prmreclem5  16860  rami  16955  ramub1lem1  16966  ramub1lem2  16967  prmgaplem3  16993  prmgaplem4  16994  prmgaplem5  16995  prmgaplem6  16996  ismre  17521  ismri  17566  isacs  17586  isacs1i  17592  catlid  17618  catrid  17619  ismon  17669  isnat  17886  eldmcoa  18001  fncnvimaeqv  18055  lubeldm  18286  glbeldm  18299  gsumval2  18623  ismgmhm  18633  issubmgm  18639  rabsubmgmd  18641  mgmhmeql  18653  ismhm  18722  issubm  18740  issubmd  18743  mndind  18765  grplinv  18931  issubg  19068  isnsg  19096  cycsubg  19149  isgim  19203  isga  19232  elcntz  19263  elcntzsn  19266  symgfix2  19357  symgsssg  19408  symgfisg  19409  psgnunilem5  19435  odid  19479  odlem2  19480  gexid  19522  gexlem2  19523  gexdvds  19525  isslw  19549  pgpssslw  19555  pj1id  19640  oddvdssubg  19796  pgpfac1lem5  20022  ablfaclem2  20029  isirred  20367  isrnghm  20389  isrngim  20393  isrim0  20430  issubrng  20492  issubrg  20516  rgspnmin  20560  issdrg  20733  isabv  20756  islss  20897  islmhm  20991  islmim  21026  islbs  21040  psgndiflemB  21567  elocv  21635  isobs  21687  dsmmelbas  21706  frlmelbas  21723  islinds  21776  gsumbagdiaglem  21898  rhmpsrlem2  21909  psrlidm  21929  psrridm  21930  psrass1  21931  psrcom  21935  mplsubglem  21966  mpllsslem  21967  evlsval2  22054  ismhp  22095  ismhp3  22097  mhpmulcl  22104  psdmul  22121  coe1ae0  22169  coe1mul2  22223  dmatel  22449  scmatel  22461  scmateALT  22468  symgmatr01lem  22609  pmatcoe1fsupp  22657  cpmatel  22667  chpscmat  22798  istopon  22868  fctop  22960  cctop  22962  ppttop  22963  pptbas  22964  epttop  22965  iscld  22983  clscld  23003  isnei  23059  neips  23069  neiptopnei  23088  iscn  23191  iscnp  23193  cmpsublem  23355  conncompconn  23388  2ndc1stc  23407  2ndcdisj  23412  elkgen  23492  xkoccn  23575  txdis1cn  23591  txkgen  23608  xkococnlem  23615  xkococn  23616  xkoinjcn  23643  txconn  23645  elqtop  23653  elmptrab  23783  fbssfi  23793  opnfbas  23798  elfg  23827  cfinfil  23849  csdfil  23850  supfil  23851  filssufilg  23867  uffix  23877  fixufil  23878  uffixfr  23879  elflim2  23920  fclscf  23981  flimfnfcls  23984  alexsubALTlem2  24004  alexsubALTlem4  24006  alexsubALT  24007  ptcmplem2  24009  elutop  24189  isucn  24233  iscfilu  24243  ispsmet  24260  ismet  24279  isxmet  24280  elblps  24343  elbl  24344  restmetu  24526  icccmp  24782  elcncf  24850  ishtpy  24939  isphtpy  24948  om1elbas  25000  iscfil  25233  iscau  25244  iscmet  25252  lmle  25269  rrxfsupp  25370  minveclem3  25397  minveclem4  25400  ovolshftlem1  25478  ovolscalem1  25482  ovolicc2lem3  25488  dyadmax  25567  dyadmbllem  25568  opnmbllem  25570  vitalilem2  25578  vitalilem3  25579  elcpn  25904  ig1pval3  26151  coelem  26199  quotlem  26276  elqaalem1  26295  elqaalem3  26297  aannenlem1  26304  aannenlem2  26305  dmarea  26935  jensen  26967  ftalem4  27054  efnnfsumcl  27081  efchtdvds  27137  sqff1o  27160  fsumdvdsdiaglem  27161  dvdsppwf1o  27164  dvdsflf1o  27165  dvdsflsumcom  27166  musum  27169  muinv  27171  logfac2  27196  dchrelbas  27215  lgsfle1  27285  lgsle1  27291  lgsdirprm  27310  lgsne0  27314  lgsquadlem1  27359  lgsquadlem2  27360  dchrvmasumlem1  27474  logsqvma  27521  pntleml  27590  ltsval2  27636  ltsres  27642  conway  27787  cutcuts  27789  cutbday  27792  cutsun12  27798  cutbdaybnd2  27804  cutbdaylt  27806  bday1  27822  cutlt  27940  precsexlem8  28222  precsexlem9  28223  precsexlem11  28225  oncutlt  28272  noseqinds  28301  peano5uzs  28412  uzsind  28413  tgellng  28637  mircgr  28741  mirbtwn  28742  iseqlg  28951  ttgelitv  28967  upgrle  29175  upgrbi  29178  umgredg2  29185  umgrbi  29186  edgupgr  29219  edgumgr  29220  upgredg  29222  numedglnl  29229  edgusgr  29245  usgruspgrb  29268  usgredg2ALT  29278  ushgredgedg  29314  ushgredgedgloop  29316  usgrexmplef  29344  upgrreslem  29389  umgrreslem  29390  upgrres1  29398  nbgrel  29425  nbupgrel  29430  nbumgrvtx  29431  nbusgreledg  29438  nbgrnself  29444  uvtxusgrel  29488  vtxdgoddnumeven  29639  rgrusgrprc  29675  lfgrwlkprop  29771  iswwlks  29921  iswwlksn  29923  wwlksnextsurj  29985  rusgrnumwwlkslem  30057  rusgrnumwwlks  30062  isclwwlk  30071  clwwlknscsh  30149  eleclclwwlkn  30163  clwlknf1oclwwlkn  30171  clwwlkvbij  30200  eupth2lems  30325  konigsberglem4  30342  fusgreg2wsplem  30420  2clwwlkel  30436  extwwlkfabel  30440  clwwlknonclwlknonf1o  30449  dlwwlknondlwlknonf1o  30452  numclwwlk2lem1  30463  numclwlk2lem2f  30464  numclwlk2lem2f1o  30466  grpoidinv2  30603  grpoinv  30613  isssp  30812  islno  30841  isblo  30870  ishmo  30899  ubthlem1  30958  ubthlem2  30959  htthlem  31005  ocel  31369  shsval2i  31475  ococin  31496  chsupsn  31501  eleigvec  32045  cnlnadjlem5  32159  shatomistici  32449  hatomistici  32450  dmrab  32583  elrabrd  32585  nnindf  32911  indf1ofs  32959  ismnt  33076  pwrssmgc  33093  tocycf  33211  tocyc01  33212  trsp2cyc  33217  cycpmco2f1  33218  cycpmco2rn  33219  cycpmco2lem2  33221  cycpmco2lem3  33222  cycpmco2lem5  33224  cycpmco2lem6  33225  cycpmco2lem7  33226  cycpmconjv  33236  tocyccntz  33238  cyc3evpm  33244  cycpmgcl  33247  cycpmconjslem2  33249  cyc3conja  33251  isfxp  33262  fxpgaeq  33263  elrgspnsubrun  33343  fldgensdrg  33408  nsgmgclem  33504  nsgmgc  33505  nsgqusf1olem2  33507  isprmidl  33531  ismxidl  33555  ssmxidl  33567  isrprm  33610  1arithufdlem3  33639  1arithufdlem4  33640  1arithufd  33641  mplvrpmlem  33720  mplvrpmga  33722  mplvrpmmhm  33723  fedgmullem2  33808  ply1annnr  33881  minplyann  33887  minplyirred  33889  constrsuc  33916  zarclsiin  34049  zart0  34057  rhmpreimacnlem  34062  ordtconnlem1  34102  sigagenval  34318  ldsysgenld  34338  ldgenpisyslem1  34341  ldgenpisyslem2  34342  ldgenpisys  34344  ddemeas  34414  ismbfm  34429  imambfm  34440  dya2iocuni  34461  oms0  34475  omssubadd  34478  elcarsg  34483  issibf  34511  sitgfval  34519  oddpwdc  34532  eulerpartlemgh  34556  eulerpartlemgs2  34558  dstfrvel  34652  ballotlemfc0  34671  ballotlemfcc  34672  ballotlemiex  34680  ballotlemfrcn0  34708  ballotlemirc  34710  ballotlem7  34714  reprsum  34791  reprsuc  34793  reprpmtf1o  34804  reprdifc  34805  fnrelpredd  35268  fineqvnttrclselem2  35300  connpconn  35451  iscvm  35475  cvmsi  35481  cvmsval  35482  cvmliftmolem2  35498  cvmliftiota  35517  snmlval  35547  satfv1lem  35578  fmlafvel  35601  fmla1  35603  fmlaomn0  35606  satfv0fvfmla0  35629  sategoelfvb  35635  elmpst  35752  lineelsb2  36364  linerflx1  36365  fwddifval  36378  fwddifnval  36379  rankeq1o  36387  finminlem  36534  fneint  36564  fnessref  36573  topmeet  36580  topjoin  36581  neifg  36587  weiunlem  36679  weiunfrlem  36680  weiunse  36684  regsfromregtr  36690  relowlssretop  37618  fin2solem  37857  fin2so  37858  poimirlem4  37875  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  poimirlem31  37902  poimirlem32  37903  opnmbllem0  37907  mblfinlem2  37909  itg2gt0cn  37926  indexa  37984  nninfnub  38002  istotbnd  38020  sstotbnd2  38025  isbnd  38031  isrngohom  38216  isrngoiso  38229  isidl  38265  ispridl  38285  ismaxidl  38291  prnc  38318  isfldidl  38319  islshp  39355  lssats  39388  islfl  39436  isat  39662  atlatmstc  39695  islln  39882  islpln  39906  islvol  39949  linepsubN  40128  elpmap  40134  pmapsub  40144  elpadd  40175  paddvaln0N  40177  islhp  40372  isldil  40486  isltrn  40495  isdilN  40530  istrnN  40533  diaval  41408  diaelval  41409  diaeldm  41412  diaelrnN  41421  cdlemm10N  41494  docaclN  41500  dibglbN  41542  dicval  41552  dicfnN  41559  dicvalrelN  41561  dihglblem2aN  41669  dihglblem2N  41670  dihglblem3N  41671  dih1dimatlem  41705  dihglb2  41718  dochvalr  41733  doch2val2  41740  dochocss  41742  islpolN  41859  mapd0  42041  aks4d1p4  42449  aks4d1p7  42453  isprimroot  42463  linvh  42466  primrootsunit1  42467  primrootscoprmpow  42469  primrootscoprbij  42472  sticksstones3  42518  aks6d1c6lem3  42542  grpods  42564  unitscyglem2  42566  unitscyglem4  42568  unitscyglem5  42569  supinf  42612  fsuppssindlem2  42950  infdesc  43001  isnacs  43061  elmzpcl  43083  mzpindd  43103  rencldnfilem  43177  irrapxlem6  43184  pellexlem3  43188  pellexlem5  43190  elpell1qr  43204  elpell14qr  43206  elpell1234qr  43208  pellfundre  43238  pellfundge  43239  pellfundlb  43241  pellfundglb  43242  rmspecnonsq  43264  jm2.22  43352  jm2.23  43353  rpnnen3lem  43388  fnwe2lem2  43408  elmnc  43493  dgraalem  43502  dgraaub  43505  mpaalem  43509  onsucelab  43620  limnsuc  43622  sqrtcvallem1  43987  rfovcnvf1od  44360  scottelrankd  44603  nzss  44673  iccshift  45878  iooshift  45882  limcperiod  45988  sumnnodd  45990  ioodvbdlimc1lem1  46289  dvnprodlem1  46304  dvnprodlem3  46306  itgperiod  46339  stoweidlem14  46372  stoweidlem15  46373  stoweidlem16  46374  stoweidlem31  46389  stoweidlem36  46394  stoweidlem46  46404  stoweidlem48  46406  fourierdlem2  46467  fourierdlem3  46468  fourierdlem20  46485  fourierdlem25  46490  fourierdlem37  46502  fourierdlem42  46507  fourierdlem48  46512  fourierdlem51  46515  fourierdlem63  46527  fourierdlem64  46528  fourierdlem65  46529  fourierdlem79  46543  fourierdlem81  46545  elaa2lem  46591  etransclem24  46616  etransclem26  46618  etransclem28  46620  etransclem35  46627  etransclem48  46640  salgenval  46679  salgenn0  46689  salgencl  46690  sssalgen  46693  salgenss  46694  salgenuni  46695  issalgend  46696  salgencntex  46701  subsaliuncllem  46715  sge0fodjrnlem  46774  meadjiunlem  46823  caragenel  46853  ovnlecvr  46916  ovnpnfelsup  46917  ovncvrrp  46922  ovnsubaddlem1  46928  hoidmv1lelem1  46949  hoidmv1lelem2  46950  hoidmv1lelem3  46951  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem4  46956  ovnhoilem1  46959  ovnlecvr2  46968  ovncvr2  46969  issmflem  47085  smflimlem2  47130  smflimlem3  47131  smflimsuplem2  47179  elsetpreimafvrab  47754  iccpart  47776  sprel  47844  prelspr  47846  sprsymrelfolem2  47853  sprsymrelf  47855  prpair  47861  paireqne  47871  prprelb  47876  prprelprb  47877  dfodd2  47996  dfeven5  48026  dfodd7  48027  fpprel  48088  clnbgrel  48188  clnbupgrel  48194  sclnbgrel  48207  vopnbgrel  48214  dfclnbgr6  48216  dfnbgr6  48217  isubgredg  48226  uhgrimisgrgric  48291  grtriprop  48301  isgrtri  48303  stgredgel  48317  stgrusgra  48319  uspgrlimlem3  48350  uspgrlim  48352  grlimgredgex  48360  grlimgrtrilem2  48362  gpgiedgdmel  48409  gpgedgel  48410  gpgnbgrvtx0  48434  gpgnbgrvtx1  48435  gpgprismgr4cycllem10  48464  1hegrlfgr  48492  assintop  48569  isassintop  48570  assintopcllaw  48572  0even  48597  2even  48599  2zrngamgm  48605  dmatALTbasel  48762  lcoval  48772  elbigo  48911  elrrx2linest2  49105  itsclc0  49131  itsclc0b  49132  itscnhlinecirc02p  49145  unilbss  49177  secval  50106  cscval  50107  cotval  50108