Theorem elrab 3650

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {crab 3416  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457

This theorem is referenced by:  elrab3  3651  elrabd  3652  elrabrd  3653  elrab2  3654  ralrab  3657  rexrab  3659  reurab  3664  rabsnt  4697  unimax  4910  ssintub  4931  intminss  4939  rabxfrd  5388  ssimaex  6966  weniso  7352  canth  7364  riotarab  7409  sorpsscmpl  7731  onnminsb  7794  dfom2  7860  ssnlim  7878  elsuppfng  8161  elsuppfn  8162  ressuppssdif  8177  oeeulem  8583  cofonr  8656  elpmg  8836  fineqvlem  9222  mapfienlem2  9362  supub  9415  suplub  9416  ordtypelem6  9481  ordtypelem7  9482  hartogslem1  9500  hartogs  9502  wemapsolem  9508  card2on  9512  elharval  9519  wdom2d  9538  cantnfs  9631  scottex  9855  scottelrankd  9869  tskwe  9932  cardid2  9935  iscard2  9958  cardmin2  9981  acni3  10027  alephsuc2  10060  kmlem1  10130  cofsmo  10248  coftr  10252  fin23lem11  10296  enfin2i  10300  fin1a2lem9  10387  fin1a2lem11  10389  axcc4  10418  axdc3lem2  10430  zorn2lem7  10481  ondomon  10542  alephval2  10552  grutsk  10802  negf1o  11639  infm3  12169  nnind  12246  peano2uz2  12679  peano5uzi  12680  dfuzi  12682  uzind  12683  uzind3  12685  eluz1  12861  uzind4  12925  nnwos  12934  eqreznegel  12953  zmin  12963  elixx1  13376  elioo2  13408  elfz1  13535  flval3  13844  serge0  14088  expge0  14130  expge1  14131  hashbclem  14485  pr2pwpr  14512  elss2prb  14521  hash2sspr  14522  wrdmap  14579  wwlktovfo  14991  shftf  15112  rlimrege0  15626  incexc2  15888  dvdsdivcl  16369  divalglem4  16449  divalgmod  16459  bitsval  16477  bezout  16596  dfgcd2  16599  lcmledvds  16652  lcmgcdlem  16659  lcmfledvds  16685  1nprm  16732  1idssfct  16733  isprm2  16735  hashdvds  16829  phisum  16845  odzval  16846  odzcllem  16847  odzdvds  16850  prmreclem2  16972  prmreclem5  16975  rami  17070  ramub1lem1  17081  ramub1lem2  17082  prmgaplem3  17108  prmgaplem4  17109  prmgaplem5  17110  prmgaplem6  17111  ismre  17637  ismri  17682  isacs  17702  isacs1i  17708  catlid  17734  catrid  17735  ismon  17785  isnat  18002  eldmcoa  18117  fncnvimaeqv  18171  lubeldm  18402  glbeldm  18415  gsumval2  18739  ismgmhm  18749  issubmgm  18755  rabsubmgmd  18757  mgmhmeql  18769  ismhm  18838  issubm  18856  issubmd  18859  mndind  18882  grplinv  19051  issubg  19187  isnsg  19216  cycsubg  19274  isgim  19327  isga  19356  elcntz  19387  elcntzsn  19390  symgfix2  19481  symgsssg  19532  symgfisg  19533  psgnunilem5  19559  odid  19603  odlem2  19604  gexid  19646  gexlem2  19647  gexdvds  19649  isslw  19673  pgpssslw  19679  pj1id  19764  oddvdssubg  19920  pgpfac1lem5  20146  ablfaclem2  20153  isirred  20497  isrnghm  20519  isrngim  20523  isrhm0  20554  isrim0  20561  rimval  20578  issubrng  20646  issubrg  20670  rgspnmin  20714  issdrg  20891  isabv  20914  islss  21055  islmhm  21148  islmim  21183  islbs  21197  isprmidl  21463  psgndiflemB  21750  elocv  21818  isobs  21870  dsmmelbas  21889  frlmelbas  21906  islinds  21959  gsumbagdiaglem  22081  rhmpsrlem2  22091  psrlidm  22111  psrridm  22112  psrass1  22113  psrcom  22117  mplsubglem  22148  mpllsslem  22149  evlsval2  22238  ismhp  22303  ismhp3  22305  mhpmulcl  22312  psdmul  22329  coe1ae0  22376  coe1mul2  22430  dmatel  22650  scmatel  22662  scmateALT  22669  symgmatr01lem  22810  pmatcoe1fsupp  22858  cpmatel  22868  chpscmat  22999  istopon  23069  fctop  23161  cctop  23163  ppttop  23164  pptbas  23165  epttop  23166  iscld  23184  clscld  23204  isnei  23260  neips  23270  neiptopnei  23289  iscn  23392  iscnp  23394  cmpsublem  23556  conncompconn  23589  2ndc1stc  23608  2ndcdisj  23613  elkgen  23693  xkoccn  23776  txdis1cn  23792  txkgen  23809  xkococnlem  23816  xkococn  23817  xkoinjcn  23844  txconn  23846  elqtop  23854  elmptrab  23984  fbssfi  23994  opnfbas  23999  elfg  24028  cfinfil  24050  csdfil  24051  supfil  24052  filssufilg  24068  uffix  24078  fixufil  24079  uffixfr  24080  elflim2  24121  fclscf  24182  flimfnfcls  24185  alexsubALTlem2  24205  alexsubALTlem4  24207  alexsubALT  24208  ptcmplem2  24210  elutop  24390  isucn  24434  iscfilu  24444  ispsmet  24461  ismet  24480  isxmet  24481  elblps  24544  elbl  24545  restmetu  24727  icccmp  24983  elcncf  25048  ishtpy  25131  isphtpy  25140  om1elbas  25191  iscfil  25424  iscau  25435  iscmet  25443  lmle  25460  rrxfsupp  25561  minveclem3  25588  minveclem4  25591  ovolshftlem1  25668  ovolscalem1  25672  ovolicc2lem3  25678  dyadmax  25757  dyadmbllem  25758  opnmbllem  25760  vitalilem2  25768  vitalilem3  25769  elcpn  26093  ig1pval3  26335  coelem  26383  quotlem  26461  elqaalem1  26480  elqaalem3  26482  aannenlem1  26491  aannenlem2  26492  dmarea  27122  jensen  27153  ftalem4  27240  efnnfsumcl  27267  efchtdvds  27323  sqff1o  27346  fsumdvdsdiaglem  27347  dvdsppwf1o  27350  dvdsflf1o  27351  dvdsflsumcom  27352  musum  27355  muinv  27357  logfac2  27381  dchrelbas  27400  lgsfle1  27470  lgsle1  27476  lgsdirprm  27495  lgsne0  27499  lgsquadlem1  27544  lgsquadlem2  27545  dchrvmasumlem1  27659  logsqvma  27706  pntleml  27775  ltsval2  27820  ltsres  27826  conway  27972  cutcuts  27974  cutbday  27977  cutsun12  27983  cutbdaybnd2  27989  cutbdaylt  27991  bday1  28007  cutlt  28125  precsexlem8  28407  precsexlem9  28408  precsexlem11  28410  oncutlt  28457  noseqinds  28486  peano5uzs  28597  uzsind  28598  tgellng  28822  mircgr  28934  mirbtwn  28935  elplng  29062  iseqlg  29184  ttgelitv  29232  upgrle  29440  upgrbi  29443  umgredg2  29450  umgrbi  29451  edgupgr  29484  edgumgr  29485  upgredg  29487  numedglnl  29494  edgusgr  29510  usgruspgrb  29533  usgredg2ALT  29543  ushgredgedg  29579  ushgredgedgloop  29581  usgrexmplef  29609  upgrreslem  29654  umgrreslem  29655  upgrres1  29663  nbgrel  29690  nbupgrel  29695  nbumgrvtx  29696  nbusgreledg  29703  nbgrnself  29709  uvtxusgrel  29753  vtxdgoddnumeven  29903  rgrusgrprc  29939  lfgrwlkprop  30035  iswwlks  30185  iswwlksn  30187  wwlksnextsurj  30249  rusgrnumwwlkslem  30321  rusgrnumwwlks  30326  isclwwlk  30335  clwwlknscsh  30413  eleclclwwlkn  30427  clwlknf1oclwwlkn  30435  clwwlkvbij  30464  eupth2lems  30589  konigsberglem4  30606  fusgreg2wsplem  30684  2clwwlkel  30700  extwwlkfabel  30704  clwwlknonclwlknonf1o  30713  dlwwlknondlwlknonf1o  30716  numclwwlk2lem1  30727  numclwlk2lem2f  30728  numclwlk2lem2f1o  30730  grpoidinv2  30867  grpoinv  30877  isssp  31076  islno  31105  isblo  31134  ishmo  31163  ubthlem1  31222  ubthlem2  31223  htthlem  31269  ocel  31633  shsval2i  31739  ococin  31760  chsupsn  31765  eleigvec  32309  cnlnadjlem5  32423  shatomistici  32713  hatomistici  32714  dmrab  32843  nnindf  33164  indf1ofs  33186  ismnt  33303  pwrssmgc  33320  tocycf  33437  tocyc01  33438  trsp2cyc  33443  cycpmco2f1  33444  cycpmco2rn  33445  cycpmco2lem2  33447  cycpmco2lem3  33448  cycpmco2lem5  33450  cycpmco2lem6  33451  cycpmco2lem7  33452  cycpmconjv  33462  tocyccntz  33464  cyc3evpm  33470  cycpmgcl  33473  cyc3conja  33477  isfxp  33488  fxpgaeq  33489  elrgspnsubrun  33569  rlocisunit  33596  fldgensdrg  33635  nsgmgclem  33720  nsgmgc  33721  nsgqusf1olem2  33723  ismxidl  33745  ssmxidl  33757  isrprm  33807  1arithufdlem3  33836  1arithufdlem4  33837  1arithufd  33838  mplvrpmlem  33933  mplvrpmga  33935  mplvrpmmhm  33936  fedgmullem2  34020  ply1annnr  34093  minplyann  34099  minplyirred  34101  constrsuc  34128  zarclsiin  34261  zart0  34269  rhmpreimacnlem  34274  ordtconnlem1  34314  sigagenval  34530  ldsysgenld  34550  ldgenpisyslem1  34553  ldgenpisyslem2  34554  ldgenpisys  34556  ddemeas  34626  ismbfm  34641  imambfm  34652  dya2iocuni  34673  oms0  34687  omssubadd  34690  elcarsg  34695  issibf  34723  sitgfval  34731  oddpwdc  34744  eulerpartlemgh  34768  eulerpartlemgs2  34770  dstfrvel  34864  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemiex  34892  ballotlemfrcn0  34920  ballotlemirc  34922  ballotlem7  34926  reprsum  35000  reprsuc  35002  reprpmtf1o  35013  reprdifc  35014  fnrelpredd  35482  fineqvnttrclselem2  35535  connpconn  35727  iscvm  35751  cvmsi  35757  cvmsval  35758  cvmliftmolem2  35774  cvmliftiota  35793  snmlval  35823  satfv1lem  35854  fmlafvel  35877  fmla1  35879  fmlaomn0  35882  satfv0fvfmla0  35905  sategoelfvb  35911  elmpst  36028  lineelsb2  36640  linerflx1  36641  fwddifval  36654  fwddifnval  36655  rankeq1o  36663  finminlem  36829  fneint  36859  fnessref  36868  topmeet  36875  topjoin  36876  neifg  36882  weiunlem  36974  weiunfrlem  36975  weiunse  36979  regsfromregtco  37049  relowlssretop  38009  fin2solem  38257  fin2so  38258  poimirlem4  38275  poimirlem25  38296  poimirlem26  38297  poimirlem27  38298  poimirlem31  38302  poimirlem32  38303  opnmbllem0  38307  mblfinlem2  38309  itg2gt0cn  38326  indexa  38384  nninfnub  38402  istotbnd  38420  sstotbnd2  38425  isbnd  38431  isrngohom  38616  isrngoiso  38629  isidl  38665  ispridl  38685  ismaxidl  38691  prnc  38718  isfldidl  38719  islshp  39753  lssats  39786  islfl  39834  isat  40060  atlatmstc  40093  islln  40280  islpln  40304  islvol  40347  linepsubN  40526  elpmap  40532  pmapsub  40542  elpadd  40573  paddvaln0N  40575  islhp  40770  isldil  40884  isltrn  40893  isdilN  40928  istrnN  40931  diaval  41806  diaelval  41807  diaeldm  41810  diaelrnN  41819  cdlemm10N  41892  docaclN  41898  dibglbN  41940  dicval  41950  dicfnN  41957  dicvalrelN  41959  dihglblem2aN  42067  dihglblem2N  42068  dihglblem3N  42069  dih1dimatlem  42103  dihglb2  42116  dochvalr  42131  doch2val2  42138  dochocss  42140  islpolN  42257  mapd0  42439  aks4d1p4  42846  aks4d1p7  42850  isprimroot  42860  linvh  42863  primrootsunit1  42864  primrootscoprmpow  42866  primrootscoprbij  42869  sticksstones3  42915  aks6d1c6lem3  42939  grpods  42961  unitscyglem2  42963  unitscyglem4  42965  unitscyglem5  42966  supinf  43010  fsuppssindlem2  43324  infdesc  43375  isnacs  43435  elmzpcl  43457  mzpindd  43477  rencldnfilem  43547  irrapxlem6  43554  pellexlem3  43558  pellexlem5  43560  elpell1qr  43574  elpell14qr  43576  elpell1234qr  43578  pellfundre  43608  pellfundge  43609  pellfundlb  43611  pellfundglb  43612  rmspecnonsq  43634  jm2.22  43722  jm2.23  43723  rpnnen3lem  43758  fnwe2lem2  43778  elmnc  43863  dgraalem  43872  dgraaub  43875  mpaalem  43879  onsucelab  43990  limnsuc  43992  sqrtcvallem1  44357  rfovcnvf1od  44730  nzss  45027  iccshift  46234  iooshift  46238  limcperiod  46344  sumnnodd  46346  ioodvbdlimc1lem1  46645  dvnprodlem1  46660  dvnprodlem3  46662  itgperiod  46695  stoweidlem14  46728  stoweidlem15  46729  stoweidlem16  46730  stoweidlem31  46745  stoweidlem36  46750  stoweidlem46  46760  stoweidlem48  46762  fourierdlem2  46823  fourierdlem3  46824  fourierdlem20  46841  fourierdlem25  46846  fourierdlem37  46858  fourierdlem42  46863  fourierdlem48  46868  fourierdlem51  46871  fourierdlem63  46883  fourierdlem64  46884  fourierdlem65  46885  fourierdlem79  46899  fourierdlem81  46901  elaa2lem  46947  etransclem24  46972  etransclem26  46974  etransclem28  46976  etransclem35  46983  etransclem48  46996  salgenval  47035  salgenn0  47045  salgencl  47046  sssalgen  47049  salgenss  47050  salgenuni  47051  issalgend  47052  salgencntex  47057  subsaliuncllem  47071  sge0fodjrnlem  47130  meadjiunlem  47179  caragenel  47209  ovnlecvr  47272  ovnpnfelsup  47273  ovncvrrp  47278  ovnsubaddlem1  47284  hoidmv1lelem1  47305  hoidmv1lelem2  47306  hoidmv1lelem3  47307  hoidmvlelem1  47309  hoidmvlelem2  47310  hoidmvlelem4  47312  ovnhoilem1  47315  ovnlecvr2  47324  ovncvr2  47325  issmflem  47441  smflimlem2  47486  smflimlem3  47487  smflimsuplem2  47535  elsetpreimafvrab  48143  iccpart  48165  sprel  48233  prelspr  48235  sprsymrelfolem2  48242  sprsymrelf  48244  prpair  48250  paireqne  48260  prprelb  48265  prprelprb  48266  dfodd2  48401  dfeven5  48431  dfodd7  48432  fpprel  48493  clnbgrel  48593  clnbupgrel  48599  sclnbgrel  48612  vopnbgrel  48619  dfclnbgr6  48621  dfnbgr6  48622  isubgredg  48631  uhgrimisgrgric  48696  grtriprop  48706  isgrtri  48708  stgredgel  48722  stgrusgra  48724  uspgrlimlem3  48755  uspgrlim  48757  grlimgredgex  48765  grlimgrtrilem2  48767  gpgiedgdmel  48814  gpgedgel  48815  gpgnbgrvtx0  48839  gpgnbgrvtx1  48840  gpgprismgr4cycllem10  48869  1hegrlfgr  48897  assintop  48974  isassintop  48975  assintopcllaw  48977  0even  49002  2even  49004  2zrngamgm  49010  dmatALTbasel  49182  lcoval  49192  elbigo  49331  elrrx2linest2  49525  itsclc0  49551  itsclc0b  49552  itscnhlinecirc02p  49565  unilbss  49596  secval  50525  cscval  50526  cotval  50527