Theorem elrab 3656

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

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

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 3403  df-v 3446

This theorem is referenced by:  elrab3  3657  elrabd  3658  elrab2  3659  ralrab  3662  rexrab  3664  reurab  3669  rabsnt  4691  unimax  4904  ssintub  4926  intminss  4934  rabxfrd  5367  ssimaex  6928  weniso  7311  canth  7323  riotarab  7368  sorpsscmpl  7690  onnminsb  7755  dfom2  7824  ssnlim  7842  elsuppfng  8125  elsuppfn  8126  ressuppssdif  8141  oeeulem  8542  cofonr  8615  elpmg  8793  fineqvlem  9185  mapfienlem2  9333  supub  9386  suplub  9387  ordtypelem6  9452  ordtypelem7  9453  hartogslem1  9471  hartogs  9473  wemapsolem  9479  card2on  9483  elharval  9490  wdom2d  9509  cantnfs  9595  scottex  9814  tskwe  9879  cardid2  9882  iscard2  9905  cardmin2  9928  acni3  9976  alephsuc2  10009  kmlem1  10080  cofsmo  10198  coftr  10202  fin23lem11  10246  enfin2i  10250  fin1a2lem9  10337  fin1a2lem11  10339  axcc4  10368  axdc3lem2  10380  zorn2lem7  10431  ondomon  10492  alephval2  10501  grutsk  10751  negf1o  11584  infm3  12118  nnind  12180  peano2uz2  12598  peano5uzi  12599  dfuzi  12601  uzind  12602  uzind3  12604  eluz1  12773  uzind4  12841  nnwos  12850  eqreznegel  12869  zmin  12879  elixx1  13291  elioo2  13323  elfz1  13449  flval3  13753  serge0  13997  expge0  14039  expge1  14040  hashbclem  14393  pr2pwpr  14420  elss2prb  14429  hash2sspr  14430  wrdmap  14487  wwlktovfo  14900  shftf  15021  rlimrege0  15521  incexc2  15780  dvdsdivcl  16262  divalglem4  16342  divalgmod  16352  bitsval  16370  bezout  16489  dfgcd2  16492  lcmledvds  16545  lcmgcdlem  16552  lcmfledvds  16578  1nprm  16625  1idssfct  16626  isprm2  16628  hashdvds  16721  phisum  16737  odzval  16738  odzcllem  16739  odzdvds  16742  prmreclem2  16864  prmreclem5  16867  rami  16962  ramub1lem1  16973  ramub1lem2  16974  prmgaplem3  17000  prmgaplem4  17001  prmgaplem5  17002  prmgaplem6  17003  ismre  17527  ismri  17568  isacs  17588  isacs1i  17594  catlid  17620  catrid  17621  ismon  17671  isnat  17888  eldmcoa  18003  fncnvimaeqv  18057  lubeldm  18288  glbeldm  18301  gsumval2  18589  ismgmhm  18599  issubmgm  18605  rabsubmgmd  18607  mgmhmeql  18619  ismhm  18688  issubm  18706  issubmd  18709  mndind  18731  grplinv  18897  issubg  19034  isnsg  19063  cycsubg  19116  isgim  19170  isga  19199  elcntz  19230  elcntzsn  19233  symgfix2  19322  symgsssg  19373  symgfisg  19374  psgnunilem5  19400  odid  19444  odlem2  19445  gexid  19487  gexlem2  19488  gexdvds  19490  isslw  19514  pgpssslw  19520  pj1id  19605  oddvdssubg  19761  pgpfac1lem5  19987  ablfaclem2  19994  isirred  20304  isrnghm  20326  isrngim  20330  isrim0OLD  20366  isrim0  20368  issubrng  20432  issubrg  20456  rgspnmin  20500  issdrg  20673  isabv  20696  islss  20816  islmhm  20910  islmim  20945  islbs  20959  psgndiflemB  21485  elocv  21553  isobs  21605  dsmmelbas  21624  frlmelbas  21641  islinds  21694  gsumbagdiaglem  21815  rhmpsrlem2  21826  psrlidm  21847  psrridm  21848  psrass1  21849  psrcom  21853  mplsubglem  21884  mpllsslem  21885  evlsval2  21970  ismhp  22003  ismhp3  22005  mhpmulcl  22012  psdmul  22029  coe1ae0  22077  coe1mul2  22131  dmatel  22356  scmatel  22368  scmateALT  22375  symgmatr01lem  22516  pmatcoe1fsupp  22564  cpmatel  22574  chpscmat  22705  istopon  22775  fctop  22867  cctop  22869  ppttop  22870  pptbas  22871  epttop  22872  iscld  22890  clscld  22910  isnei  22966  neips  22976  neiptopnei  22995  iscn  23098  iscnp  23100  cmpsublem  23262  conncompconn  23295  2ndc1stc  23314  2ndcdisj  23319  elkgen  23399  xkoccn  23482  txdis1cn  23498  txkgen  23515  xkococnlem  23522  xkococn  23523  xkoinjcn  23550  txconn  23552  elqtop  23560  elmptrab  23690  fbssfi  23700  opnfbas  23705  elfg  23734  cfinfil  23756  csdfil  23757  supfil  23758  filssufilg  23774  uffix  23784  fixufil  23785  uffixfr  23786  elflim2  23827  fclscf  23888  flimfnfcls  23891  alexsubALTlem2  23911  alexsubALTlem4  23913  alexsubALT  23914  ptcmplem2  23916  elutop  24097  isucn  24141  iscfilu  24151  ispsmet  24168  ismet  24187  isxmet  24188  elblps  24251  elbl  24252  restmetu  24434  icccmp  24690  elcncf  24758  ishtpy  24847  isphtpy  24856  om1elbas  24908  iscfil  25141  iscau  25152  iscmet  25160  lmle  25177  rrxfsupp  25278  minveclem3  25305  minveclem4  25308  ovolshftlem1  25386  ovolscalem1  25390  ovolicc2lem3  25396  dyadmax  25475  dyadmbllem  25476  opnmbllem  25478  vitalilem2  25486  vitalilem3  25487  elcpn  25812  ig1pval3  26059  coelem  26107  quotlem  26184  elqaalem1  26203  elqaalem3  26205  aannenlem1  26212  aannenlem2  26213  dmarea  26843  jensen  26875  ftalem4  26962  efnnfsumcl  26989  efchtdvds  27045  sqff1o  27068  fsumdvdsdiaglem  27069  dvdsppwf1o  27072  dvdsflf1o  27073  dvdsflsumcom  27074  musum  27077  muinv  27079  logfac2  27104  dchrelbas  27123  lgsfle1  27193  lgsle1  27199  lgsdirprm  27218  lgsne0  27222  lgsquadlem1  27267  lgsquadlem2  27268  dchrvmasumlem1  27382  logsqvma  27429  pntleml  27498  sltval2  27544  sltres  27550  conway  27687  scutcut  27689  scutbday  27692  scutun12  27698  scutbdaybnd2  27704  scutbdaylt  27706  bday1s  27719  cutlt  27816  precsexlem8  28092  precsexlem9  28093  precsexlem11  28095  onscutlt  28141  noseqinds  28163  peano5uzs  28268  uzsind  28269  tgellng  28456  mircgr  28560  mirbtwn  28561  iseqlg  28770  ttgelitv  28786  upgrle  28993  upgrbi  28996  umgredg2  29003  umgrbi  29004  edgupgr  29037  edgumgr  29038  upgredg  29040  numedglnl  29047  edgusgr  29063  usgruspgrb  29086  usgredg2ALT  29096  ushgredgedg  29132  ushgredgedgloop  29134  usgrexmplef  29162  upgrreslem  29207  umgrreslem  29208  upgrres1  29216  nbgrel  29243  nbupgrel  29248  nbumgrvtx  29249  nbusgreledg  29256  nbgrnself  29262  uvtxusgrel  29306  vtxdgoddnumeven  29457  rgrusgrprc  29493  lfgrwlkprop  29589  iswwlks  29739  iswwlksn  29741  wwlksnextsurj  29803  rusgrnumwwlkslem  29872  rusgrnumwwlks  29877  isclwwlk  29886  clwwlknscsh  29964  eleclclwwlkn  29978  clwlknf1oclwwlkn  29986  clwwlkvbij  30015  eupth2lems  30140  konigsberglem4  30157  fusgreg2wsplem  30235  2clwwlkel  30251  extwwlkfabel  30255  clwwlknonclwlknonf1o  30264  dlwwlknondlwlknonf1o  30267  numclwwlk2lem1  30278  numclwlk2lem2f  30279  numclwlk2lem2f1o  30281  grpoidinv2  30417  grpoinv  30427  isssp  30626  islno  30655  isblo  30684  ishmo  30713  ubthlem1  30772  ubthlem2  30773  htthlem  30819  ocel  31183  shsval2i  31289  ococin  31310  chsupsn  31315  eleigvec  31859  cnlnadjlem5  31973  shatomistici  32263  hatomistici  32264  dmrab  32399  nnindf  32717  indf1ofs  32762  ismnt  32882  pwrssmgc  32899  tocycf  33047  tocyc01  33048  trsp2cyc  33053  cycpmco2f1  33054  cycpmco2rn  33055  cycpmco2lem2  33057  cycpmco2lem3  33058  cycpmco2lem5  33060  cycpmco2lem6  33061  cycpmco2lem7  33062  cycpmconjv  33072  tocyccntz  33074  cyc3evpm  33080  cycpmgcl  33083  cycpmconjslem2  33085  cyc3conja  33087  isfxp  33098  fxpgaeq  33099  elrgspnsubrun  33173  fldgensdrg  33237  nsgmgclem  33355  nsgmgc  33356  nsgqusf1olem2  33358  isprmidl  33382  ismxidl  33406  ssmxidl  33418  isrprm  33461  1arithufdlem3  33490  1arithufdlem4  33491  1arithufd  33492  fedgmullem2  33599  ply1annnr  33666  minplyann  33672  minplyirred  33674  constrsuc  33701  zarclsiin  33834  zart0  33842  rhmpreimacnlem  33847  ordtconnlem1  33887  sigagenval  34103  ldsysgenld  34123  ldgenpisyslem1  34126  ldgenpisyslem2  34127  ldgenpisys  34129  ddemeas  34199  ismbfm  34214  imambfm  34226  dya2iocuni  34247  oms0  34261  omssubadd  34264  elcarsg  34269  issibf  34297  sitgfval  34305  oddpwdc  34318  eulerpartlemgh  34342  eulerpartlemgs2  34344  dstfrvel  34438  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemiex  34466  ballotlemfrcn0  34494  ballotlemirc  34496  ballotlem7  34500  reprsum  34577  reprsuc  34579  reprpmtf1o  34590  reprdifc  34591  fnrelpredd  35052  connpconn  35195  iscvm  35219  cvmsi  35225  cvmsval  35226  cvmliftmolem2  35242  cvmliftiota  35261  snmlval  35291  satfv1lem  35322  fmlafvel  35345  fmla1  35347  fmlaomn0  35350  satfv0fvfmla0  35373  sategoelfvb  35379  elmpst  35496  lineelsb2  36109  linerflx1  36110  fwddifval  36123  fwddifnval  36124  rankeq1o  36132  finminlem  36279  fneint  36309  fnessref  36318  topmeet  36325  topjoin  36326  neifg  36332  weiunlem2  36424  weiunfrlem  36425  weiunse  36429  relowlssretop  37324  fin2solem  37573  fin2so  37574  poimirlem4  37591  poimirlem25  37612  poimirlem26  37613  poimirlem27  37614  poimirlem31  37618  poimirlem32  37619  opnmbllem0  37623  mblfinlem2  37625  itg2gt0cn  37642  indexa  37700  nninfnub  37718  istotbnd  37736  sstotbnd2  37741  isbnd  37747  isrngohom  37932  isrngoiso  37945  isidl  37981  ispridl  38001  ismaxidl  38007  prnc  38034  isfldidl  38035  islshp  38945  lssats  38978  islfl  39026  isat  39252  atlatmstc  39285  islln  39473  islpln  39497  islvol  39540  linepsubN  39719  elpmap  39725  pmapsub  39735  elpadd  39766  paddvaln0N  39768  islhp  39963  isldil  40077  isltrn  40086  isdilN  40121  istrnN  40124  diaval  40999  diaelval  41000  diaeldm  41003  diaelrnN  41012  cdlemm10N  41085  docaclN  41091  dibglbN  41133  dicval  41143  dicfnN  41150  dicvalrelN  41152  dihglblem2aN  41260  dihglblem2N  41261  dihglblem3N  41262  dih1dimatlem  41296  dihglb2  41309  dochvalr  41324  doch2val2  41331  dochocss  41333  islpolN  41450  mapd0  41632  aks4d1p4  42040  aks4d1p7  42044  isprimroot  42054  linvh  42057  primrootsunit1  42058  primrootscoprmpow  42060  primrootscoprbij  42063  sticksstones3  42109  aks6d1c6lem3  42133  grpods  42155  unitscyglem2  42157  unitscyglem4  42159  unitscyglem5  42160  supinf  42203  fsuppssindlem2  42553  infdesc  42604  isnacs  42665  elmzpcl  42687  mzpindd  42707  rencldnfilem  42781  irrapxlem6  42788  pellexlem3  42792  pellexlem5  42794  elpell1qr  42808  elpell14qr  42810  elpell1234qr  42812  pellfundre  42842  pellfundge  42843  pellfundlb  42845  pellfundglb  42846  rmspecnonsq  42868  jm2.22  42957  jm2.23  42958  rpnnen3lem  42993  fnwe2lem2  43013  elmnc  43098  dgraalem  43107  dgraaub  43110  mpaalem  43114  onsucelab  43225  limnsuc  43227  sqrtcvallem1  43593  rfovcnvf1od  43966  scottelrankd  44209  nzss  44279  iccshift  45489  iooshift  45493  limcperiod  45599  sumnnodd  45601  ioodvbdlimc1lem1  45902  dvnprodlem1  45917  dvnprodlem3  45919  itgperiod  45952  stoweidlem14  45985  stoweidlem15  45986  stoweidlem16  45987  stoweidlem31  46002  stoweidlem36  46007  stoweidlem46  46017  stoweidlem48  46019  fourierdlem2  46080  fourierdlem3  46081  fourierdlem20  46098  fourierdlem25  46103  fourierdlem37  46115  fourierdlem42  46120  fourierdlem48  46125  fourierdlem51  46128  fourierdlem63  46140  fourierdlem64  46141  fourierdlem65  46142  fourierdlem79  46156  fourierdlem81  46158  elaa2lem  46204  etransclem24  46229  etransclem26  46231  etransclem28  46233  etransclem35  46240  etransclem48  46253  salgenval  46292  salgenn0  46302  salgencl  46303  sssalgen  46306  salgenss  46307  salgenuni  46308  issalgend  46309  salgencntex  46314  subsaliuncllem  46328  sge0fodjrnlem  46387  meadjiunlem  46436  caragenel  46466  ovnlecvr  46529  ovnpnfelsup  46530  ovncvrrp  46535  ovnsubaddlem1  46541  hoidmv1lelem1  46562  hoidmv1lelem2  46563  hoidmv1lelem3  46564  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem4  46569  ovnhoilem1  46572  ovnlecvr2  46581  ovncvr2  46582  issmflem  46698  smflimlem2  46743  smflimlem3  46744  smflimsuplem2  46792  elsetpreimafvrab  47368  iccpart  47390  sprel  47458  prelspr  47460  sprsymrelfolem2  47467  sprsymrelf  47469  prpair  47475  paireqne  47485  prprelb  47490  prprelprb  47491  dfodd2  47610  dfeven5  47640  dfodd7  47641  fpprel  47702  clnbgrel  47802  clnbupgrel  47808  sclnbgrel  47820  vopnbgrel  47827  dfclnbgr6  47829  dfnbgr6  47830  isubgredg  47839  uhgrimisgrgric  47904  grtriprop  47913  isgrtri  47915  stgredgel  47929  stgrusgra  47931  uspgrlimlem3  47962  uspgrlim  47964  grlimgrtrilem1  47966  grlimgrtrilem2  47967  gpgiedgdmel  48013  gpgedgel  48014  gpgnbgrvtx0  48038  gpgnbgrvtx1  48039  gpgprismgr4cycllem10  48067  1hegrlfgr  48093  assintop  48170  isassintop  48171  assintopcllaw  48173  0even  48198  2even  48200  2zrngamgm  48206  dmatALTbasel  48364  lcoval  48374  elbigo  48513  elrrx2linest2  48707  itsclc0  48733  itsclc0b  48734  itscnhlinecirc02p  48747  unilbss  48779  secval  49709  cscval  49710  cotval  49711