Theorem elrab 3694

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {crab 3432  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479

This theorem is referenced by:  elrab3  3695  elrabd  3696  elrab2  3697  ralrab  3701  rexrab  3704  reurab  3709  rabsnt  4735  unimax  4948  ssintub  4970  intminss  4978  rabxfrd  5422  ssimaex  6993  weniso  7373  canth  7384  riotarab  7429  sorpsscmpl  7752  onnminsb  7818  dfom2  7888  ssnlim  7906  elsuppfng  8192  elsuppfn  8193  ressuppssdif  8208  oeeulem  8637  cofonr  8710  elpmg  8881  fineqvlem  9295  mapfienlem2  9443  supub  9496  suplub  9497  ordtypelem6  9560  ordtypelem7  9561  hartogslem1  9579  hartogs  9581  wemapsolem  9587  card2on  9591  elharval  9598  wdom2d  9617  cantnfs  9703  scottex  9922  tskwe  9987  cardid2  9990  iscard2  10013  cardmin2  10036  acni3  10084  alephsuc2  10117  kmlem1  10188  cofsmo  10306  coftr  10310  fin23lem11  10354  enfin2i  10358  fin1a2lem9  10445  fin1a2lem11  10447  axcc4  10476  axdc3lem2  10488  zorn2lem7  10539  ondomon  10600  alephval2  10609  grutsk  10859  negf1o  11690  infm3  12224  nnind  12281  peano2uz2  12703  peano5uzi  12704  dfuzi  12706  uzind  12707  uzind3  12709  eluz1  12879  uzind4  12945  nnwos  12954  eqreznegel  12973  zmin  12983  elixx1  13392  elioo2  13424  elfz1  13548  flval3  13851  serge0  14093  expge0  14135  expge1  14136  hashbclem  14487  pr2pwpr  14514  elss2prb  14523  hash2sspr  14524  wrdmap  14580  wwlktovfo  14993  shftf  15114  rlimrege0  15611  incexc2  15870  dvdsdivcl  16349  divalglem4  16429  divalgmod  16439  bitsval  16457  bezout  16576  dfgcd2  16579  lcmledvds  16632  lcmgcdlem  16639  lcmfledvds  16665  1nprm  16712  1idssfct  16713  isprm2  16715  hashdvds  16808  phisum  16823  odzval  16824  odzcllem  16825  odzdvds  16828  prmreclem2  16950  prmreclem5  16953  rami  17048  ramub1lem1  17059  ramub1lem2  17060  prmgaplem3  17086  prmgaplem4  17087  prmgaplem5  17088  prmgaplem6  17089  ismre  17634  ismri  17675  isacs  17695  isacs1i  17701  catlid  17727  catrid  17728  ismon  17780  isnat  18001  eldmcoa  18118  fncnvimaeqv  18174  lubeldm  18410  glbeldm  18423  gsumval2  18711  ismgmhm  18721  issubmgm  18727  rabsubmgmd  18729  mgmhmeql  18741  ismhm  18810  issubm  18828  issubmd  18831  mndind  18853  grplinv  19019  issubg  19156  isnsg  19185  cycsubg  19238  isgim  19292  isga  19321  elcntz  19352  elcntzsn  19355  symgfix2  19448  symgsssg  19499  symgfisg  19500  psgnunilem5  19526  odid  19570  odlem2  19571  gexid  19613  gexlem2  19614  gexdvds  19616  isslw  19640  pgpssslw  19646  pj1id  19731  oddvdssubg  19887  pgpfac1lem5  20113  ablfaclem2  20120  isirred  20435  isrnghm  20457  isrngim  20461  isrim0OLD  20497  isrim0  20499  issubrng  20563  issubrg  20587  rgspnmin  20631  issdrg  20805  isabv  20828  islss  20949  islmhm  21043  islmim  21078  islbs  21092  psgndiflemB  21635  elocv  21703  isobs  21757  dsmmelbas  21776  frlmelbas  21793  islinds  21846  gsumbagdiaglem  21967  rhmpsrlem2  21978  psrlidm  21999  psrridm  22000  psrass1  22001  psrcom  22005  mplsubglem  22036  mpllsslem  22037  evlsval2  22128  ismhp  22161  ismhp3  22163  mhpmulcl  22170  psdmul  22187  coe1ae0  22233  coe1mul2  22287  dmatel  22514  scmatel  22526  scmateALT  22533  symgmatr01lem  22674  pmatcoe1fsupp  22722  cpmatel  22732  chpscmat  22863  istopon  22933  fctop  23026  cctop  23028  ppttop  23029  pptbas  23030  epttop  23031  iscld  23050  clscld  23070  isnei  23126  neips  23136  neiptopnei  23155  iscn  23258  iscnp  23260  cmpsublem  23422  conncompconn  23455  2ndc1stc  23474  2ndcdisj  23479  elkgen  23559  xkoccn  23642  txdis1cn  23658  txkgen  23675  xkococnlem  23682  xkococn  23683  xkoinjcn  23710  txconn  23712  elqtop  23720  elmptrab  23850  fbssfi  23860  opnfbas  23865  elfg  23894  cfinfil  23916  csdfil  23917  supfil  23918  filssufilg  23934  uffix  23944  fixufil  23945  uffixfr  23946  elflim2  23987  fclscf  24048  flimfnfcls  24051  alexsubALTlem2  24071  alexsubALTlem4  24073  alexsubALT  24074  ptcmplem2  24076  elutop  24257  isucn  24302  iscfilu  24312  ispsmet  24329  ismet  24348  isxmet  24349  elblps  24412  elbl  24413  restmetu  24598  icccmp  24860  elcncf  24928  ishtpy  25017  isphtpy  25026  om1elbas  25078  iscfil  25312  iscau  25323  iscmet  25331  lmle  25348  rrxfsupp  25449  minveclem3  25476  minveclem4  25479  ovolshftlem1  25557  ovolscalem1  25561  ovolicc2lem3  25567  dyadmax  25646  dyadmbllem  25647  opnmbllem  25649  vitalilem2  25657  vitalilem3  25658  elcpn  25984  ig1pval3  26231  coelem  26279  quotlem  26356  elqaalem1  26375  elqaalem3  26377  aannenlem1  26384  aannenlem2  26385  dmarea  27014  jensen  27046  ftalem4  27133  efnnfsumcl  27160  efchtdvds  27216  sqff1o  27239  fsumdvdsdiaglem  27240  dvdsppwf1o  27243  dvdsflf1o  27244  dvdsflsumcom  27245  musum  27248  muinv  27250  logfac2  27275  dchrelbas  27294  lgsfle1  27364  lgsle1  27370  lgsdirprm  27389  lgsne0  27393  lgsquadlem1  27438  lgsquadlem2  27439  dchrvmasumlem1  27553  logsqvma  27600  pntleml  27669  sltval2  27715  sltres  27721  conway  27858  scutcut  27860  scutbday  27863  scutun12  27869  scutbdaybnd2  27875  scutbdaylt  27877  bday1s  27890  cutlt  27980  precsexlem8  28252  precsexlem9  28253  precsexlem11  28255  noseqinds  28313  peano5uzs  28404  uzsind  28405  tgellng  28575  mircgr  28679  mirbtwn  28680  iseqlg  28889  ttgelitv  28911  upgrle  29121  upgrbi  29124  umgredg2  29131  umgrbi  29132  edgupgr  29165  edgumgr  29166  upgredg  29168  numedglnl  29175  edgusgr  29191  usgruspgrb  29214  usgredg2ALT  29224  ushgredgedg  29260  ushgredgedgloop  29262  usgrexmplef  29290  upgrreslem  29335  umgrreslem  29336  upgrres1  29344  nbgrel  29371  nbupgrel  29376  nbumgrvtx  29377  nbusgreledg  29384  nbgrnself  29390  uvtxusgrel  29434  vtxdgoddnumeven  29585  rgrusgrprc  29621  lfgrwlkprop  29719  iswwlks  29865  iswwlksn  29867  wwlksnextsurj  29929  rusgrnumwwlkslem  29998  rusgrnumwwlks  30003  isclwwlk  30012  clwwlknscsh  30090  eleclclwwlkn  30104  clwlknf1oclwwlkn  30112  clwwlkvbij  30141  eupth2lems  30266  konigsberglem4  30283  fusgreg2wsplem  30361  2clwwlkel  30377  extwwlkfabel  30381  clwwlknonclwlknonf1o  30390  dlwwlknondlwlknonf1o  30393  numclwwlk2lem1  30404  numclwlk2lem2f  30405  numclwlk2lem2f1o  30407  grpoidinv2  30543  grpoinv  30553  isssp  30752  islno  30781  isblo  30810  ishmo  30839  ubthlem1  30898  ubthlem2  30899  htthlem  30945  ocel  31309  shsval2i  31415  ococin  31436  chsupsn  31441  eleigvec  31985  cnlnadjlem5  32099  shatomistici  32389  hatomistici  32390  dmrab  32524  nnindf  32825  ismnt  32957  pwrssmgc  32974  tocycf  33119  tocyc01  33120  trsp2cyc  33125  cycpmco2f1  33126  cycpmco2rn  33127  cycpmco2lem2  33129  cycpmco2lem3  33130  cycpmco2lem5  33132  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmconjv  33144  tocyccntz  33146  cyc3evpm  33152  cycpmgcl  33155  cycpmconjslem2  33157  cyc3conja  33159  fldgensdrg  33295  nsgmgclem  33418  nsgmgc  33419  nsgqusf1olem2  33421  isprmidl  33445  ismxidl  33469  ssmxidl  33481  isrprm  33524  1arithufdlem3  33553  1arithufdlem4  33554  1arithufd  33555  fedgmullem2  33657  ply1annnr  33710  minplyann  33716  minplyirred  33718  constrsuc  33742  zarclsiin  33831  zart0  33839  rhmpreimacnlem  33844  ordtconnlem1  33884  indf1ofs  34006  sigagenval  34120  ldsysgenld  34140  ldgenpisyslem1  34143  ldgenpisyslem2  34144  ldgenpisys  34146  ddemeas  34216  ismbfm  34231  imambfm  34243  dya2iocuni  34264  oms0  34278  omssubadd  34281  elcarsg  34286  issibf  34314  sitgfval  34322  oddpwdc  34335  eulerpartlemgh  34359  eulerpartlemgs2  34361  dstfrvel  34454  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemiex  34482  ballotlemfrcn0  34510  ballotlemirc  34512  ballotlem7  34516  reprsum  34606  reprsuc  34608  reprpmtf1o  34619  reprdifc  34620  fnrelpredd  35081  connpconn  35219  iscvm  35243  cvmsi  35249  cvmsval  35250  cvmliftmolem2  35266  cvmliftiota  35285  snmlval  35315  satfv1lem  35346  fmlafvel  35369  fmla1  35371  fmlaomn0  35374  satfv0fvfmla0  35397  sategoelfvb  35403  elmpst  35520  lineelsb2  36129  linerflx1  36130  fwddifval  36143  fwddifnval  36144  rankeq1o  36152  finminlem  36300  fneint  36330  fnessref  36339  topmeet  36346  topjoin  36347  neifg  36353  weiunlem2  36445  weiunfrlem  36446  weiunse  36450  relowlssretop  37345  fin2solem  37592  fin2so  37593  poimirlem4  37610  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem31  37637  poimirlem32  37638  opnmbllem0  37642  mblfinlem2  37644  itg2gt0cn  37661  indexa  37719  nninfnub  37737  istotbnd  37755  sstotbnd2  37760  isbnd  37766  isrngohom  37951  isrngoiso  37964  isidl  38000  ispridl  38020  ismaxidl  38026  prnc  38053  isfldidl  38054  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  42060  aks4d1p7  42064  isprimroot  42074  linvh  42077  primrootsunit1  42078  primrootscoprmpow  42080  primrootscoprbij  42083  sticksstones3  42129  aks6d1c6lem3  42153  grpods  42175  unitscyglem2  42177  unitscyglem4  42179  unitscyglem5  42180  supinf  42261  fsuppssindlem2  42578  infdesc  42629  isnacs  42691  elmzpcl  42713  mzpindd  42733  rencldnfilem  42807  irrapxlem6  42814  pellexlem3  42818  pellexlem5  42820  elpell1qr  42834  elpell14qr  42836  elpell1234qr  42838  pellfundre  42868  pellfundge  42869  pellfundlb  42871  pellfundglb  42872  rmspecnonsq  42894  jm2.22  42983  jm2.23  42984  rpnnen3lem  43019  fnwe2lem2  43039  elmnc  43124  dgraalem  43133  dgraaub  43136  mpaalem  43140  onsucelab  43252  limnsuc  43254  sqrtcvallem1  43620  rfovcnvf1od  43993  scottelrankd  44242  nzss  44312  iccshift  45470  iooshift  45474  limcperiod  45583  sumnnodd  45585  ioodvbdlimc1lem1  45886  dvnprodlem1  45901  dvnprodlem3  45903  itgperiod  45936  stoweidlem14  45969  stoweidlem15  45970  stoweidlem16  45971  stoweidlem31  45986  stoweidlem36  45991  stoweidlem46  46001  stoweidlem48  46003  fourierdlem2  46064  fourierdlem3  46065  fourierdlem20  46082  fourierdlem25  46087  fourierdlem37  46099  fourierdlem42  46104  fourierdlem48  46109  fourierdlem51  46112  fourierdlem63  46124  fourierdlem64  46125  fourierdlem65  46126  fourierdlem79  46140  fourierdlem81  46142  elaa2lem  46188  etransclem24  46213  etransclem26  46215  etransclem28  46217  etransclem35  46224  etransclem48  46237  salgenval  46276  salgenn0  46286  salgencl  46287  sssalgen  46290  salgenss  46291  salgenuni  46292  issalgend  46293  salgencntex  46298  subsaliuncllem  46312  sge0fodjrnlem  46371  meadjiunlem  46420  caragenel  46450  ovnlecvr  46513  ovnpnfelsup  46514  ovncvrrp  46519  ovnsubaddlem1  46525  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem4  46553  ovnhoilem1  46556  ovnlecvr2  46565  ovncvr2  46566  issmflem  46682  smflimlem2  46727  smflimlem3  46728  smflimsuplem2  46776  elsetpreimafvrab  47318  iccpart  47340  sprel  47408  prelspr  47410  sprsymrelfolem2  47417  sprsymrelf  47419  prpair  47425  paireqne  47435  prprelb  47440  prprelprb  47441  dfodd2  47560  dfeven5  47590  dfodd7  47591  fpprel  47652  clnbgrel  47752  clnbupgrel  47758  sclnbgrel  47770  vopnbgrel  47777  dfclnbgr6  47779  dfnbgr6  47780  isubgredg  47789  uhgrimisgrgric  47836  grtriprop  47845  isgrtri  47847  stgredgel  47859  stgrusgra  47861  uspgrlimlem3  47892  uspgrlim  47894  grlimgrtrilem1  47896  grlimgrtrilem2  47897  gpgedgel  47942  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  1hegrlfgr  47975  assintop  48052  isassintop  48053  assintopcllaw  48055  0even  48080  2even  48082  2zrngamgm  48088  dmatALTbasel  48247  lcoval  48257  elbigo  48400  elrrx2linest2  48594  itsclc0  48620  itsclc0b  48621  itscnhlinecirc02p  48634  unilbss  48665  secval  48977  cscval  48978  cotval  48979