Theorem elrab 3659

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 3468	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} → 𝐴 ∈ V)
2		elex 3468	. . 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 3406	. . 3 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜑)}
8	6, 7	elab2g 3647	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
9	1, 3, 8	pm5.21nii 378	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

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

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 3406  df-v 3449

This theorem is referenced by:  elrab3  3660  elrabd  3661  elrab2  3662  ralrab  3665  rexrab  3667  reurab  3672  rabsnt  4695  unimax  4908  ssintub  4930  intminss  4938  rabxfrd  5372  ssimaex  6946  weniso  7329  canth  7341  riotarab  7386  sorpsscmpl  7710  onnminsb  7775  dfom2  7844  ssnlim  7862  elsuppfng  8148  elsuppfn  8149  ressuppssdif  8164  oeeulem  8565  cofonr  8638  elpmg  8816  fineqvlem  9209  mapfienlem2  9357  supub  9410  suplub  9411  ordtypelem6  9476  ordtypelem7  9477  hartogslem1  9495  hartogs  9497  wemapsolem  9503  card2on  9507  elharval  9514  wdom2d  9533  cantnfs  9619  scottex  9838  tskwe  9903  cardid2  9906  iscard2  9929  cardmin2  9952  acni3  10000  alephsuc2  10033  kmlem1  10104  cofsmo  10222  coftr  10226  fin23lem11  10270  enfin2i  10274  fin1a2lem9  10361  fin1a2lem11  10363  axcc4  10392  axdc3lem2  10404  zorn2lem7  10455  ondomon  10516  alephval2  10525  grutsk  10775  negf1o  11608  infm3  12142  nnind  12204  peano2uz2  12622  peano5uzi  12623  dfuzi  12625  uzind  12626  uzind3  12628  eluz1  12797  uzind4  12865  nnwos  12874  eqreznegel  12893  zmin  12903  elixx1  13315  elioo2  13347  elfz1  13473  flval3  13777  serge0  14021  expge0  14063  expge1  14064  hashbclem  14417  pr2pwpr  14444  elss2prb  14453  hash2sspr  14454  wrdmap  14511  wwlktovfo  14924  shftf  15045  rlimrege0  15545  incexc2  15804  dvdsdivcl  16286  divalglem4  16366  divalgmod  16376  bitsval  16394  bezout  16513  dfgcd2  16516  lcmledvds  16569  lcmgcdlem  16576  lcmfledvds  16602  1nprm  16649  1idssfct  16650  isprm2  16652  hashdvds  16745  phisum  16761  odzval  16762  odzcllem  16763  odzdvds  16766  prmreclem2  16888  prmreclem5  16891  rami  16986  ramub1lem1  16997  ramub1lem2  16998  prmgaplem3  17024  prmgaplem4  17025  prmgaplem5  17026  prmgaplem6  17027  ismre  17551  ismri  17592  isacs  17612  isacs1i  17618  catlid  17644  catrid  17645  ismon  17695  isnat  17912  eldmcoa  18027  fncnvimaeqv  18081  lubeldm  18312  glbeldm  18325  gsumval2  18613  ismgmhm  18623  issubmgm  18629  rabsubmgmd  18631  mgmhmeql  18643  ismhm  18712  issubm  18730  issubmd  18733  mndind  18755  grplinv  18921  issubg  19058  isnsg  19087  cycsubg  19140  isgim  19194  isga  19223  elcntz  19254  elcntzsn  19257  symgfix2  19346  symgsssg  19397  symgfisg  19398  psgnunilem5  19424  odid  19468  odlem2  19469  gexid  19511  gexlem2  19512  gexdvds  19514  isslw  19538  pgpssslw  19544  pj1id  19629  oddvdssubg  19785  pgpfac1lem5  20011  ablfaclem2  20018  isirred  20328  isrnghm  20350  isrngim  20354  isrim0OLD  20390  isrim0  20392  issubrng  20456  issubrg  20480  rgspnmin  20524  issdrg  20697  isabv  20720  islss  20840  islmhm  20934  islmim  20969  islbs  20983  psgndiflemB  21509  elocv  21577  isobs  21629  dsmmelbas  21648  frlmelbas  21665  islinds  21718  gsumbagdiaglem  21839  rhmpsrlem2  21850  psrlidm  21871  psrridm  21872  psrass1  21873  psrcom  21877  mplsubglem  21908  mpllsslem  21909  evlsval2  21994  ismhp  22027  ismhp3  22029  mhpmulcl  22036  psdmul  22053  coe1ae0  22101  coe1mul2  22155  dmatel  22380  scmatel  22392  scmateALT  22399  symgmatr01lem  22540  pmatcoe1fsupp  22588  cpmatel  22598  chpscmat  22729  istopon  22799  fctop  22891  cctop  22893  ppttop  22894  pptbas  22895  epttop  22896  iscld  22914  clscld  22934  isnei  22990  neips  23000  neiptopnei  23019  iscn  23122  iscnp  23124  cmpsublem  23286  conncompconn  23319  2ndc1stc  23338  2ndcdisj  23343  elkgen  23423  xkoccn  23506  txdis1cn  23522  txkgen  23539  xkococnlem  23546  xkococn  23547  xkoinjcn  23574  txconn  23576  elqtop  23584  elmptrab  23714  fbssfi  23724  opnfbas  23729  elfg  23758  cfinfil  23780  csdfil  23781  supfil  23782  filssufilg  23798  uffix  23808  fixufil  23809  uffixfr  23810  elflim2  23851  fclscf  23912  flimfnfcls  23915  alexsubALTlem2  23935  alexsubALTlem4  23937  alexsubALT  23938  ptcmplem2  23940  elutop  24121  isucn  24165  iscfilu  24175  ispsmet  24192  ismet  24211  isxmet  24212  elblps  24275  elbl  24276  restmetu  24458  icccmp  24714  elcncf  24782  ishtpy  24871  isphtpy  24880  om1elbas  24932  iscfil  25165  iscau  25176  iscmet  25184  lmle  25201  rrxfsupp  25302  minveclem3  25329  minveclem4  25332  ovolshftlem1  25410  ovolscalem1  25414  ovolicc2lem3  25420  dyadmax  25499  dyadmbllem  25500  opnmbllem  25502  vitalilem2  25510  vitalilem3  25511  elcpn  25836  ig1pval3  26083  coelem  26131  quotlem  26208  elqaalem1  26227  elqaalem3  26229  aannenlem1  26236  aannenlem2  26237  dmarea  26867  jensen  26899  ftalem4  26986  efnnfsumcl  27013  efchtdvds  27069  sqff1o  27092  fsumdvdsdiaglem  27093  dvdsppwf1o  27096  dvdsflf1o  27097  dvdsflsumcom  27098  musum  27101  muinv  27103  logfac2  27128  dchrelbas  27147  lgsfle1  27217  lgsle1  27223  lgsdirprm  27242  lgsne0  27246  lgsquadlem1  27291  lgsquadlem2  27292  dchrvmasumlem1  27406  logsqvma  27453  pntleml  27522  sltval2  27568  sltres  27574  conway  27711  scutcut  27713  scutbday  27716  scutun12  27722  scutbdaybnd2  27728  scutbdaylt  27730  bday1s  27743  cutlt  27840  precsexlem8  28116  precsexlem9  28117  precsexlem11  28119  onscutlt  28165  noseqinds  28187  peano5uzs  28292  uzsind  28293  tgellng  28480  mircgr  28584  mirbtwn  28585  iseqlg  28794  ttgelitv  28810  upgrle  29017  upgrbi  29020  umgredg2  29027  umgrbi  29028  edgupgr  29061  edgumgr  29062  upgredg  29064  numedglnl  29071  edgusgr  29087  usgruspgrb  29110  usgredg2ALT  29120  ushgredgedg  29156  ushgredgedgloop  29158  usgrexmplef  29186  upgrreslem  29231  umgrreslem  29232  upgrres1  29240  nbgrel  29267  nbupgrel  29272  nbumgrvtx  29273  nbusgreledg  29280  nbgrnself  29286  uvtxusgrel  29330  vtxdgoddnumeven  29481  rgrusgrprc  29517  lfgrwlkprop  29615  iswwlks  29766  iswwlksn  29768  wwlksnextsurj  29830  rusgrnumwwlkslem  29899  rusgrnumwwlks  29904  isclwwlk  29913  clwwlknscsh  29991  eleclclwwlkn  30005  clwlknf1oclwwlkn  30013  clwwlkvbij  30042  eupth2lems  30167  konigsberglem4  30184  fusgreg2wsplem  30262  2clwwlkel  30278  extwwlkfabel  30282  clwwlknonclwlknonf1o  30291  dlwwlknondlwlknonf1o  30294  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwlk2lem2f1o  30308  grpoidinv2  30444  grpoinv  30454  isssp  30653  islno  30682  isblo  30711  ishmo  30740  ubthlem1  30799  ubthlem2  30800  htthlem  30846  ocel  31210  shsval2i  31316  ococin  31337  chsupsn  31342  eleigvec  31886  cnlnadjlem5  32000  shatomistici  32290  hatomistici  32291  dmrab  32426  nnindf  32744  indf1ofs  32789  ismnt  32909  pwrssmgc  32926  tocycf  33074  tocyc01  33075  trsp2cyc  33080  cycpmco2f1  33081  cycpmco2rn  33082  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmconjv  33099  tocyccntz  33101  cyc3evpm  33107  cycpmgcl  33110  cycpmconjslem2  33112  cyc3conja  33114  isfxp  33125  fxpgaeq  33126  elrgspnsubrun  33200  fldgensdrg  33264  nsgmgclem  33382  nsgmgc  33383  nsgqusf1olem2  33385  isprmidl  33409  ismxidl  33433  ssmxidl  33445  isrprm  33488  1arithufdlem3  33517  1arithufdlem4  33518  1arithufd  33519  fedgmullem2  33626  ply1annnr  33693  minplyann  33699  minplyirred  33701  constrsuc  33728  zarclsiin  33861  zart0  33869  rhmpreimacnlem  33874  ordtconnlem1  33914  sigagenval  34130  ldsysgenld  34150  ldgenpisyslem1  34153  ldgenpisyslem2  34154  ldgenpisys  34156  ddemeas  34226  ismbfm  34241  imambfm  34253  dya2iocuni  34274  oms0  34288  omssubadd  34291  elcarsg  34296  issibf  34324  sitgfval  34332  oddpwdc  34345  eulerpartlemgh  34369  eulerpartlemgs2  34371  dstfrvel  34465  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemiex  34493  ballotlemfrcn0  34521  ballotlemirc  34523  ballotlem7  34527  reprsum  34604  reprsuc  34606  reprpmtf1o  34617  reprdifc  34618  fnrelpredd  35079  connpconn  35222  iscvm  35246  cvmsi  35252  cvmsval  35253  cvmliftmolem2  35269  cvmliftiota  35288  snmlval  35318  satfv1lem  35349  fmlafvel  35372  fmla1  35374  fmlaomn0  35377  satfv0fvfmla0  35400  sategoelfvb  35406  elmpst  35523  lineelsb2  36136  linerflx1  36137  fwddifval  36150  fwddifnval  36151  rankeq1o  36159  finminlem  36306  fneint  36336  fnessref  36345  topmeet  36352  topjoin  36353  neifg  36359  weiunlem2  36451  weiunfrlem  36452  weiunse  36456  relowlssretop  37351  fin2solem  37600  fin2so  37601  poimirlem4  37618  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  poimirlem32  37646  opnmbllem0  37650  mblfinlem2  37652  itg2gt0cn  37669  indexa  37727  nninfnub  37745  istotbnd  37763  sstotbnd2  37768  isbnd  37774  isrngohom  37959  isrngoiso  37972  isidl  38008  ispridl  38028  ismaxidl  38034  prnc  38061  isfldidl  38062  islshp  38972  lssats  39005  islfl  39053  isat  39279  atlatmstc  39312  islln  39500  islpln  39524  islvol  39567  linepsubN  39746  elpmap  39752  pmapsub  39762  elpadd  39793  paddvaln0N  39795  islhp  39990  isldil  40104  isltrn  40113  isdilN  40148  istrnN  40151  diaval  41026  diaelval  41027  diaeldm  41030  diaelrnN  41039  cdlemm10N  41112  docaclN  41118  dibglbN  41160  dicval  41170  dicfnN  41177  dicvalrelN  41179  dihglblem2aN  41287  dihglblem2N  41288  dihglblem3N  41289  dih1dimatlem  41323  dihglb2  41336  dochvalr  41351  doch2val2  41358  dochocss  41360  islpolN  41477  mapd0  41659  aks4d1p4  42067  aks4d1p7  42071  isprimroot  42081  linvh  42084  primrootsunit1  42085  primrootscoprmpow  42087  primrootscoprbij  42090  sticksstones3  42136  aks6d1c6lem3  42160  grpods  42182  unitscyglem2  42184  unitscyglem4  42186  unitscyglem5  42187  supinf  42230  fsuppssindlem2  42580  infdesc  42631  isnacs  42692  elmzpcl  42714  mzpindd  42734  rencldnfilem  42808  irrapxlem6  42815  pellexlem3  42819  pellexlem5  42821  elpell1qr  42835  elpell14qr  42837  elpell1234qr  42839  pellfundre  42869  pellfundge  42870  pellfundlb  42872  pellfundglb  42873  rmspecnonsq  42895  jm2.22  42984  jm2.23  42985  rpnnen3lem  43020  fnwe2lem2  43040  elmnc  43125  dgraalem  43134  dgraaub  43137  mpaalem  43141  onsucelab  43252  limnsuc  43254  sqrtcvallem1  43620  rfovcnvf1od  43993  scottelrankd  44236  nzss  44306  iccshift  45516  iooshift  45520  limcperiod  45626  sumnnodd  45628  ioodvbdlimc1lem1  45929  dvnprodlem1  45944  dvnprodlem3  45946  itgperiod  45979  stoweidlem14  46012  stoweidlem15  46013  stoweidlem16  46014  stoweidlem31  46029  stoweidlem36  46034  stoweidlem46  46044  stoweidlem48  46046  fourierdlem2  46107  fourierdlem3  46108  fourierdlem20  46125  fourierdlem25  46130  fourierdlem37  46142  fourierdlem42  46147  fourierdlem48  46152  fourierdlem51  46155  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem79  46183  fourierdlem81  46185  elaa2lem  46231  etransclem24  46256  etransclem26  46258  etransclem28  46260  etransclem35  46267  etransclem48  46280  salgenval  46319  salgenn0  46329  salgencl  46330  sssalgen  46333  salgenss  46334  salgenuni  46335  issalgend  46336  salgencntex  46341  subsaliuncllem  46355  sge0fodjrnlem  46414  meadjiunlem  46463  caragenel  46493  ovnlecvr  46556  ovnpnfelsup  46557  ovncvrrp  46562  ovnsubaddlem1  46568  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem4  46596  ovnhoilem1  46599  ovnlecvr2  46608  ovncvr2  46609  issmflem  46725  smflimlem2  46770  smflimlem3  46771  smflimsuplem2  46819  elsetpreimafvrab  47395  iccpart  47417  sprel  47485  prelspr  47487  sprsymrelfolem2  47494  sprsymrelf  47496  prpair  47502  paireqne  47512  prprelb  47517  prprelprb  47518  dfodd2  47637  dfeven5  47667  dfodd7  47668  fpprel  47729  clnbgrel  47829  clnbupgrel  47835  sclnbgrel  47847  vopnbgrel  47854  dfclnbgr6  47856  dfnbgr6  47857  isubgredg  47866  uhgrimisgrgric  47931  grtriprop  47940  isgrtri  47942  stgredgel  47956  stgrusgra  47958  uspgrlimlem3  47989  uspgrlim  47991  grlimgrtrilem1  47993  grlimgrtrilem2  47994  gpgiedgdmel  48040  gpgedgel  48041  gpgnbgrvtx0  48065  gpgnbgrvtx1  48066  gpgprismgr4cycllem10  48094  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