Theorem elrab 3667

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3412  df-v 3457

This theorem is referenced by:  elrab3  3668  elrabd  3669  elrab2  3670  ralrab  3673  rexrab  3675  reurab  3680  rabsnt  4703  unimax  4916  ssintub  4938  intminss  4946  rabxfrd  5380  ssimaex  6953  weniso  7336  canth  7348  riotarab  7393  sorpsscmpl  7717  onnminsb  7782  dfom2  7852  ssnlim  7870  elsuppfng  8157  elsuppfn  8158  ressuppssdif  8173  oeeulem  8576  cofonr  8649  elpmg  8820  fineqvlem  9227  mapfienlem2  9375  supub  9428  suplub  9429  ordtypelem6  9494  ordtypelem7  9495  hartogslem1  9513  hartogs  9515  wemapsolem  9521  card2on  9525  elharval  9532  wdom2d  9551  cantnfs  9637  scottex  9856  tskwe  9921  cardid2  9924  iscard2  9947  cardmin2  9970  acni3  10018  alephsuc2  10051  kmlem1  10122  cofsmo  10240  coftr  10244  fin23lem11  10288  enfin2i  10292  fin1a2lem9  10379  fin1a2lem11  10381  axcc4  10410  axdc3lem2  10422  zorn2lem7  10473  ondomon  10534  alephval2  10543  grutsk  10793  negf1o  11624  infm3  12158  nnind  12215  peano2uz2  12638  peano5uzi  12639  dfuzi  12641  uzind  12642  uzind3  12644  eluz1  12813  uzind4  12879  nnwos  12888  eqreznegel  12907  zmin  12917  elixx1  13328  elioo2  13360  elfz1  13486  flval3  13789  serge0  14031  expge0  14073  expge1  14074  hashbclem  14427  pr2pwpr  14454  elss2prb  14463  hash2sspr  14464  wrdmap  14521  wwlktovfo  14934  shftf  15055  rlimrege0  15552  incexc2  15811  dvdsdivcl  16292  divalglem4  16372  divalgmod  16382  bitsval  16400  bezout  16519  dfgcd2  16522  lcmledvds  16575  lcmgcdlem  16582  lcmfledvds  16608  1nprm  16655  1idssfct  16656  isprm2  16658  hashdvds  16751  phisum  16767  odzval  16768  odzcllem  16769  odzdvds  16772  prmreclem2  16894  prmreclem5  16897  rami  16992  ramub1lem1  17003  ramub1lem2  17004  prmgaplem3  17030  prmgaplem4  17031  prmgaplem5  17032  prmgaplem6  17033  ismre  17557  ismri  17598  isacs  17618  isacs1i  17624  catlid  17650  catrid  17651  ismon  17701  isnat  17918  eldmcoa  18033  fncnvimaeqv  18087  lubeldm  18318  glbeldm  18331  gsumval2  18619  ismgmhm  18629  issubmgm  18635  rabsubmgmd  18637  mgmhmeql  18649  ismhm  18718  issubm  18736  issubmd  18739  mndind  18761  grplinv  18927  issubg  19064  isnsg  19093  cycsubg  19146  isgim  19200  isga  19229  elcntz  19260  elcntzsn  19263  symgfix2  19352  symgsssg  19403  symgfisg  19404  psgnunilem5  19430  odid  19474  odlem2  19475  gexid  19517  gexlem2  19518  gexdvds  19520  isslw  19544  pgpssslw  19550  pj1id  19635  oddvdssubg  19791  pgpfac1lem5  20017  ablfaclem2  20024  isirred  20334  isrnghm  20356  isrngim  20360  isrim0OLD  20396  isrim0  20398  issubrng  20462  issubrg  20486  rgspnmin  20530  issdrg  20703  isabv  20726  islss  20846  islmhm  20940  islmim  20975  islbs  20989  psgndiflemB  21515  elocv  21583  isobs  21635  dsmmelbas  21654  frlmelbas  21671  islinds  21724  gsumbagdiaglem  21845  rhmpsrlem2  21856  psrlidm  21877  psrridm  21878  psrass1  21879  psrcom  21883  mplsubglem  21914  mpllsslem  21915  evlsval2  22000  ismhp  22033  ismhp3  22035  mhpmulcl  22042  psdmul  22059  coe1ae0  22107  coe1mul2  22161  dmatel  22386  scmatel  22398  scmateALT  22405  symgmatr01lem  22546  pmatcoe1fsupp  22594  cpmatel  22604  chpscmat  22735  istopon  22805  fctop  22897  cctop  22899  ppttop  22900  pptbas  22901  epttop  22902  iscld  22920  clscld  22940  isnei  22996  neips  23006  neiptopnei  23025  iscn  23128  iscnp  23130  cmpsublem  23292  conncompconn  23325  2ndc1stc  23344  2ndcdisj  23349  elkgen  23429  xkoccn  23512  txdis1cn  23528  txkgen  23545  xkococnlem  23552  xkococn  23553  xkoinjcn  23580  txconn  23582  elqtop  23590  elmptrab  23720  fbssfi  23730  opnfbas  23735  elfg  23764  cfinfil  23786  csdfil  23787  supfil  23788  filssufilg  23804  uffix  23814  fixufil  23815  uffixfr  23816  elflim2  23857  fclscf  23918  flimfnfcls  23921  alexsubALTlem2  23941  alexsubALTlem4  23943  alexsubALT  23944  ptcmplem2  23946  elutop  24127  isucn  24171  iscfilu  24181  ispsmet  24198  ismet  24217  isxmet  24218  elblps  24281  elbl  24282  restmetu  24464  icccmp  24720  elcncf  24788  ishtpy  24877  isphtpy  24886  om1elbas  24938  iscfil  25172  iscau  25183  iscmet  25191  lmle  25208  rrxfsupp  25309  minveclem3  25336  minveclem4  25339  ovolshftlem1  25417  ovolscalem1  25421  ovolicc2lem3  25427  dyadmax  25506  dyadmbllem  25507  opnmbllem  25509  vitalilem2  25517  vitalilem3  25518  elcpn  25843  ig1pval3  26090  coelem  26138  quotlem  26215  elqaalem1  26234  elqaalem3  26236  aannenlem1  26243  aannenlem2  26244  dmarea  26874  jensen  26906  ftalem4  26993  efnnfsumcl  27020  efchtdvds  27076  sqff1o  27099  fsumdvdsdiaglem  27100  dvdsppwf1o  27103  dvdsflf1o  27104  dvdsflsumcom  27105  musum  27108  muinv  27110  logfac2  27135  dchrelbas  27154  lgsfle1  27224  lgsle1  27230  lgsdirprm  27249  lgsne0  27253  lgsquadlem1  27298  lgsquadlem2  27299  dchrvmasumlem1  27413  logsqvma  27460  pntleml  27529  sltval2  27575  sltres  27581  conway  27718  scutcut  27720  scutbday  27723  scutun12  27729  scutbdaybnd2  27735  scutbdaylt  27737  bday1s  27750  cutlt  27847  precsexlem8  28123  precsexlem9  28124  precsexlem11  28126  onscutlt  28172  noseqinds  28194  peano5uzs  28299  uzsind  28300  tgellng  28487  mircgr  28591  mirbtwn  28592  iseqlg  28801  ttgelitv  28817  upgrle  29024  upgrbi  29027  umgredg2  29034  umgrbi  29035  edgupgr  29068  edgumgr  29069  upgredg  29071  numedglnl  29078  edgusgr  29094  usgruspgrb  29117  usgredg2ALT  29127  ushgredgedg  29163  ushgredgedgloop  29165  usgrexmplef  29193  upgrreslem  29238  umgrreslem  29239  upgrres1  29247  nbgrel  29274  nbupgrel  29279  nbumgrvtx  29280  nbusgreledg  29287  nbgrnself  29293  uvtxusgrel  29337  vtxdgoddnumeven  29488  rgrusgrprc  29524  lfgrwlkprop  29622  iswwlks  29773  iswwlksn  29775  wwlksnextsurj  29837  rusgrnumwwlkslem  29906  rusgrnumwwlks  29911  isclwwlk  29920  clwwlknscsh  29998  eleclclwwlkn  30012  clwlknf1oclwwlkn  30020  clwwlkvbij  30049  eupth2lems  30174  konigsberglem4  30191  fusgreg2wsplem  30269  2clwwlkel  30285  extwwlkfabel  30289  clwwlknonclwlknonf1o  30298  dlwwlknondlwlknonf1o  30301  numclwwlk2lem1  30312  numclwlk2lem2f  30313  numclwlk2lem2f1o  30315  grpoidinv2  30451  grpoinv  30461  isssp  30660  islno  30689  isblo  30718  ishmo  30747  ubthlem1  30806  ubthlem2  30807  htthlem  30853  ocel  31217  shsval2i  31323  ococin  31344  chsupsn  31349  eleigvec  31893  cnlnadjlem5  32007  shatomistici  32297  hatomistici  32298  dmrab  32433  nnindf  32752  indf1ofs  32797  ismnt  32917  pwrssmgc  32934  tocycf  33082  tocyc01  33083  trsp2cyc  33088  cycpmco2f1  33089  cycpmco2rn  33090  cycpmco2lem2  33092  cycpmco2lem3  33093  cycpmco2lem5  33095  cycpmco2lem6  33096  cycpmco2lem7  33097  cycpmconjv  33107  tocyccntz  33109  cyc3evpm  33115  cycpmgcl  33118  cycpmconjslem2  33120  cyc3conja  33122  isfxp  33133  fxpgaeq  33134  elrgspnsubrun  33208  fldgensdrg  33272  nsgmgclem  33390  nsgmgc  33391  nsgqusf1olem2  33393  isprmidl  33417  ismxidl  33441  ssmxidl  33453  isrprm  33496  1arithufdlem3  33525  1arithufdlem4  33526  1arithufd  33527  fedgmullem2  33634  ply1annnr  33701  minplyann  33707  minplyirred  33709  constrsuc  33736  zarclsiin  33869  zart0  33877  rhmpreimacnlem  33882  ordtconnlem1  33922  sigagenval  34138  ldsysgenld  34158  ldgenpisyslem1  34161  ldgenpisyslem2  34162  ldgenpisys  34164  ddemeas  34234  ismbfm  34249  imambfm  34261  dya2iocuni  34282  oms0  34296  omssubadd  34299  elcarsg  34304  issibf  34332  sitgfval  34340  oddpwdc  34353  eulerpartlemgh  34377  eulerpartlemgs2  34379  dstfrvel  34473  ballotlemfc0  34492  ballotlemfcc  34493  ballotlemiex  34501  ballotlemfrcn0  34529  ballotlemirc  34531  ballotlem7  34535  reprsum  34612  reprsuc  34614  reprpmtf1o  34625  reprdifc  34626  fnrelpredd  35087  connpconn  35224  iscvm  35248  cvmsi  35254  cvmsval  35255  cvmliftmolem2  35271  cvmliftiota  35290  snmlval  35320  satfv1lem  35351  fmlafvel  35374  fmla1  35376  fmlaomn0  35379  satfv0fvfmla0  35402  sategoelfvb  35408  elmpst  35525  lineelsb2  36133  linerflx1  36134  fwddifval  36147  fwddifnval  36148  rankeq1o  36156  finminlem  36303  fneint  36333  fnessref  36342  topmeet  36349  topjoin  36350  neifg  36356  weiunlem2  36448  weiunfrlem  36449  weiunse  36453  relowlssretop  37348  fin2solem  37597  fin2so  37598  poimirlem4  37615  poimirlem25  37636  poimirlem26  37637  poimirlem27  37638  poimirlem31  37642  poimirlem32  37643  opnmbllem0  37647  mblfinlem2  37649  itg2gt0cn  37666  indexa  37724  nninfnub  37742  istotbnd  37760  sstotbnd2  37765  isbnd  37771  isrngohom  37956  isrngoiso  37969  isidl  38005  ispridl  38025  ismaxidl  38031  prnc  38058  isfldidl  38059  islshp  38964  lssats  38997  islfl  39045  isat  39271  atlatmstc  39304  islln  39492  islpln  39516  islvol  39559  linepsubN  39738  elpmap  39744  pmapsub  39754  elpadd  39785  paddvaln0N  39787  islhp  39982  isldil  40096  isltrn  40105  isdilN  40140  istrnN  40143  diaval  41018  diaelval  41019  diaeldm  41022  diaelrnN  41031  cdlemm10N  41104  docaclN  41110  dibglbN  41152  dicval  41162  dicfnN  41169  dicvalrelN  41171  dihglblem2aN  41279  dihglblem2N  41280  dihglblem3N  41281  dih1dimatlem  41315  dihglb2  41328  dochvalr  41343  doch2val2  41350  dochocss  41352  islpolN  41469  mapd0  41651  aks4d1p4  42059  aks4d1p7  42063  isprimroot  42073  linvh  42076  primrootsunit1  42077  primrootscoprmpow  42079  primrootscoprbij  42082  sticksstones3  42128  aks6d1c6lem3  42152  grpods  42174  unitscyglem2  42176  unitscyglem4  42178  unitscyglem5  42179  supinf  42222  fsuppssindlem2  42552  infdesc  42603  isnacs  42664  elmzpcl  42686  mzpindd  42706  rencldnfilem  42780  irrapxlem6  42787  pellexlem3  42791  pellexlem5  42793  elpell1qr  42807  elpell14qr  42809  elpell1234qr  42811  pellfundre  42841  pellfundge  42842  pellfundlb  42844  pellfundglb  42845  rmspecnonsq  42867  jm2.22  42956  jm2.23  42957  rpnnen3lem  42992  fnwe2lem2  43012  elmnc  43097  dgraalem  43106  dgraaub  43109  mpaalem  43113  onsucelab  43224  limnsuc  43226  sqrtcvallem1  43592  rfovcnvf1od  43965  scottelrankd  44208  nzss  44278  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  47350  iccpart  47372  sprel  47440  prelspr  47442  sprsymrelfolem2  47449  sprsymrelf  47451  prpair  47457  paireqne  47467  prprelb  47472  prprelprb  47473  dfodd2  47592  dfeven5  47622  dfodd7  47623  fpprel  47684  clnbgrel  47784  clnbupgrel  47790  sclnbgrel  47802  vopnbgrel  47809  dfclnbgr6  47811  dfnbgr6  47812  isubgredg  47821  uhgrimisgrgric  47886  grtriprop  47895  isgrtri  47897  stgredgel  47911  stgrusgra  47913  uspgrlimlem3  47944  uspgrlim  47946  grlimgrtrilem1  47948  grlimgrtrilem2  47949  gpgiedgdmel  47995  gpgedgel  47996  gpgnbgrvtx0  48018  gpgnbgrvtx1  48019  gpgprismgr4cycllem10  48045  1hegrlfgr  48049  assintop  48126  isassintop  48127  assintopcllaw  48129  0even  48154  2even  48156  2zrngamgm  48162  dmatALTbasel  48320  lcoval  48330  elbigo  48473  elrrx2linest2  48667  itsclc0  48693  itsclc0b  48694  itscnhlinecirc02p  48707  unilbss  48738  secval  49613  cscval  49614  cotval  49615