Theorem elrab 3635

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3390  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432

This theorem is referenced by:  elrab3  3636  elrabd  3637  elrab2  3638  ralrab  3641  rexrab  3643  reurab  3648  rabsnt  4676  unimax  4888  ssintub  4909  intminss  4917  rabxfrd  5354  ssimaex  6919  weniso  7302  canth  7314  riotarab  7359  sorpsscmpl  7681  onnminsb  7746  dfom2  7812  ssnlim  7830  elsuppfng  8112  elsuppfn  8113  ressuppssdif  8128  oeeulem  8530  cofonr  8603  elpmg  8783  fineqvlem  9169  mapfienlem2  9312  supub  9365  suplub  9366  ordtypelem6  9431  ordtypelem7  9432  hartogslem1  9450  hartogs  9452  wemapsolem  9458  card2on  9462  elharval  9469  wdom2d  9488  cantnfs  9578  scottex  9800  tskwe  9865  cardid2  9868  iscard2  9891  cardmin2  9914  acni3  9960  alephsuc2  9993  kmlem1  10064  cofsmo  10182  coftr  10186  fin23lem11  10230  enfin2i  10234  fin1a2lem9  10321  fin1a2lem11  10323  axcc4  10352  axdc3lem2  10364  zorn2lem7  10415  ondomon  10476  alephval2  10486  grutsk  10736  negf1o  11571  infm3  12106  nnind  12183  peano2uz2  12608  peano5uzi  12609  dfuzi  12611  uzind  12612  uzind3  12614  eluz1  12783  uzind4  12847  nnwos  12856  eqreznegel  12875  zmin  12885  elixx1  13298  elioo2  13330  elfz1  13457  flval3  13765  serge0  14009  expge0  14051  expge1  14052  hashbclem  14405  pr2pwpr  14432  elss2prb  14441  hash2sspr  14442  wrdmap  14499  wwlktovfo  14911  shftf  15032  rlimrege0  15532  incexc2  15794  dvdsdivcl  16276  divalglem4  16356  divalgmod  16366  bitsval  16384  bezout  16503  dfgcd2  16506  lcmledvds  16559  lcmgcdlem  16566  lcmfledvds  16592  1nprm  16639  1idssfct  16640  isprm2  16642  hashdvds  16736  phisum  16752  odzval  16753  odzcllem  16754  odzdvds  16757  prmreclem2  16879  prmreclem5  16882  rami  16977  ramub1lem1  16988  ramub1lem2  16989  prmgaplem3  17015  prmgaplem4  17016  prmgaplem5  17017  prmgaplem6  17018  ismre  17543  ismri  17588  isacs  17608  isacs1i  17614  catlid  17640  catrid  17641  ismon  17691  isnat  17908  eldmcoa  18023  fncnvimaeqv  18077  lubeldm  18308  glbeldm  18321  gsumval2  18645  ismgmhm  18655  issubmgm  18661  rabsubmgmd  18663  mgmhmeql  18675  ismhm  18744  issubm  18762  issubmd  18765  mndind  18787  grplinv  18956  issubg  19093  isnsg  19121  cycsubg  19174  isgim  19228  isga  19257  elcntz  19288  elcntzsn  19291  symgfix2  19382  symgsssg  19433  symgfisg  19434  psgnunilem5  19460  odid  19504  odlem2  19505  gexid  19547  gexlem2  19548  gexdvds  19550  isslw  19574  pgpssslw  19580  pj1id  19665  oddvdssubg  19821  pgpfac1lem5  20047  ablfaclem2  20054  isirred  20390  isrnghm  20412  isrngim  20416  isrim0  20453  issubrng  20515  issubrg  20539  rgspnmin  20583  issdrg  20756  isabv  20779  islss  20920  islmhm  21014  islmim  21049  islbs  21063  psgndiflemB  21590  elocv  21658  isobs  21710  dsmmelbas  21729  frlmelbas  21746  islinds  21799  gsumbagdiaglem  21920  rhmpsrlem2  21930  psrlidm  21950  psrridm  21951  psrass1  21952  psrcom  21956  mplsubglem  21987  mpllsslem  21988  evlsval2  22075  ismhp  22116  ismhp3  22118  mhpmulcl  22125  psdmul  22142  coe1ae0  22190  coe1mul2  22244  dmatel  22468  scmatel  22480  scmateALT  22487  symgmatr01lem  22628  pmatcoe1fsupp  22676  cpmatel  22686  chpscmat  22817  istopon  22887  fctop  22979  cctop  22981  ppttop  22982  pptbas  22983  epttop  22984  iscld  23002  clscld  23022  isnei  23078  neips  23088  neiptopnei  23107  iscn  23210  iscnp  23212  cmpsublem  23374  conncompconn  23407  2ndc1stc  23426  2ndcdisj  23431  elkgen  23511  xkoccn  23594  txdis1cn  23610  txkgen  23627  xkococnlem  23634  xkococn  23635  xkoinjcn  23662  txconn  23664  elqtop  23672  elmptrab  23802  fbssfi  23812  opnfbas  23817  elfg  23846  cfinfil  23868  csdfil  23869  supfil  23870  filssufilg  23886  uffix  23896  fixufil  23897  uffixfr  23898  elflim2  23939  fclscf  24000  flimfnfcls  24003  alexsubALTlem2  24023  alexsubALTlem4  24025  alexsubALT  24026  ptcmplem2  24028  elutop  24208  isucn  24252  iscfilu  24262  ispsmet  24279  ismet  24298  isxmet  24299  elblps  24362  elbl  24363  restmetu  24545  icccmp  24801  elcncf  24866  ishtpy  24949  isphtpy  24958  om1elbas  25009  iscfil  25242  iscau  25253  iscmet  25261  lmle  25278  rrxfsupp  25379  minveclem3  25406  minveclem4  25409  ovolshftlem1  25486  ovolscalem1  25490  ovolicc2lem3  25496  dyadmax  25575  dyadmbllem  25576  opnmbllem  25578  vitalilem2  25586  vitalilem3  25587  elcpn  25911  ig1pval3  26153  coelem  26201  quotlem  26277  elqaalem1  26296  elqaalem3  26298  aannenlem1  26305  aannenlem2  26306  dmarea  26934  jensen  26966  ftalem4  27053  efnnfsumcl  27080  efchtdvds  27136  sqff1o  27159  fsumdvdsdiaglem  27160  dvdsppwf1o  27163  dvdsflf1o  27164  dvdsflsumcom  27165  musum  27168  muinv  27170  logfac2  27194  dchrelbas  27213  lgsfle1  27283  lgsle1  27289  lgsdirprm  27308  lgsne0  27312  lgsquadlem1  27357  lgsquadlem2  27358  dchrvmasumlem1  27472  logsqvma  27519  pntleml  27588  ltsval2  27634  ltsres  27640  conway  27785  cutcuts  27787  cutbday  27790  cutsun12  27796  cutbdaybnd2  27802  cutbdaylt  27804  bday1  27820  cutlt  27938  precsexlem8  28220  precsexlem9  28221  precsexlem11  28223  oncutlt  28270  noseqinds  28299  peano5uzs  28410  uzsind  28411  tgellng  28635  mircgr  28739  mirbtwn  28740  iseqlg  28949  ttgelitv  28965  upgrle  29173  upgrbi  29176  umgredg2  29183  umgrbi  29184  edgupgr  29217  edgumgr  29218  upgredg  29220  numedglnl  29227  edgusgr  29243  usgruspgrb  29266  usgredg2ALT  29276  ushgredgedg  29312  ushgredgedgloop  29314  usgrexmplef  29342  upgrreslem  29387  umgrreslem  29388  upgrres1  29396  nbgrel  29423  nbupgrel  29428  nbumgrvtx  29429  nbusgreledg  29436  nbgrnself  29442  uvtxusgrel  29486  vtxdgoddnumeven  29637  rgrusgrprc  29673  lfgrwlkprop  29769  iswwlks  29919  iswwlksn  29921  wwlksnextsurj  29983  rusgrnumwwlkslem  30055  rusgrnumwwlks  30060  isclwwlk  30069  clwwlknscsh  30147  eleclclwwlkn  30161  clwlknf1oclwwlkn  30169  clwwlkvbij  30198  eupth2lems  30323  konigsberglem4  30340  fusgreg2wsplem  30418  2clwwlkel  30434  extwwlkfabel  30438  clwwlknonclwlknonf1o  30447  dlwwlknondlwlknonf1o  30450  numclwwlk2lem1  30461  numclwlk2lem2f  30462  numclwlk2lem2f1o  30464  grpoidinv2  30601  grpoinv  30611  isssp  30810  islno  30839  isblo  30868  ishmo  30897  ubthlem1  30956  ubthlem2  30957  htthlem  31003  ocel  31367  shsval2i  31473  ococin  31494  chsupsn  31499  eleigvec  32043  cnlnadjlem5  32157  shatomistici  32447  hatomistici  32448  dmrab  32581  elrabrd  32583  nnindf  32908  indf1ofs  32941  ismnt  33058  pwrssmgc  33075  tocycf  33193  tocyc01  33194  trsp2cyc  33199  cycpmco2f1  33200  cycpmco2rn  33201  cycpmco2lem2  33203  cycpmco2lem3  33204  cycpmco2lem5  33206  cycpmco2lem6  33207  cycpmco2lem7  33208  cycpmconjv  33218  tocyccntz  33220  cyc3evpm  33226  cycpmgcl  33229  cycpmconjslem2  33231  cyc3conja  33233  isfxp  33244  fxpgaeq  33245  elrgspnsubrun  33325  fldgensdrg  33390  nsgmgclem  33486  nsgmgc  33487  nsgqusf1olem2  33489  isprmidl  33513  ismxidl  33537  ssmxidl  33549  isrprm  33592  1arithufdlem3  33621  1arithufdlem4  33622  1arithufd  33623  mplvrpmlem  33702  mplvrpmga  33704  mplvrpmmhm  33705  fedgmullem2  33790  ply1annnr  33863  minplyann  33869  minplyirred  33871  constrsuc  33898  zarclsiin  34031  zart0  34039  rhmpreimacnlem  34044  ordtconnlem1  34084  sigagenval  34300  ldsysgenld  34320  ldgenpisyslem1  34323  ldgenpisyslem2  34324  ldgenpisys  34326  ddemeas  34396  ismbfm  34411  imambfm  34422  dya2iocuni  34443  oms0  34457  omssubadd  34460  elcarsg  34465  issibf  34493  sitgfval  34501  oddpwdc  34514  eulerpartlemgh  34538  eulerpartlemgs2  34540  dstfrvel  34634  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemiex  34662  ballotlemfrcn0  34690  ballotlemirc  34692  ballotlem7  34696  reprsum  34773  reprsuc  34775  reprpmtf1o  34786  reprdifc  34787  fnrelpredd  35250  fineqvnttrclselem2  35282  connpconn  35433  iscvm  35457  cvmsi  35463  cvmsval  35464  cvmliftmolem2  35480  cvmliftiota  35499  snmlval  35529  satfv1lem  35560  fmlafvel  35583  fmla1  35585  fmlaomn0  35588  satfv0fvfmla0  35611  sategoelfvb  35617  elmpst  35734  lineelsb2  36346  linerflx1  36347  fwddifval  36360  fwddifnval  36361  rankeq1o  36369  finminlem  36516  fneint  36546  fnessref  36555  topmeet  36562  topjoin  36563  neifg  36569  weiunlem  36661  weiunfrlem  36662  weiunse  36666  regsfromregtco  36736  relowlssretop  37693  fin2solem  37941  fin2so  37942  poimirlem4  37959  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  poimirlem31  37986  poimirlem32  37987  opnmbllem0  37991  mblfinlem2  37993  itg2gt0cn  38010  indexa  38068  nninfnub  38086  istotbnd  38104  sstotbnd2  38109  isbnd  38115  isrngohom  38300  isrngoiso  38313  isidl  38349  ispridl  38369  ismaxidl  38375  prnc  38402  isfldidl  38403  islshp  39439  lssats  39472  islfl  39520  isat  39746  atlatmstc  39779  islln  39966  islpln  39990  islvol  40033  linepsubN  40212  elpmap  40218  pmapsub  40228  elpadd  40259  paddvaln0N  40261  islhp  40456  isldil  40570  isltrn  40579  isdilN  40614  istrnN  40617  diaval  41492  diaelval  41493  diaeldm  41496  diaelrnN  41505  cdlemm10N  41578  docaclN  41584  dibglbN  41626  dicval  41636  dicfnN  41643  dicvalrelN  41645  dihglblem2aN  41753  dihglblem2N  41754  dihglblem3N  41755  dih1dimatlem  41789  dihglb2  41802  dochvalr  41817  doch2val2  41824  dochocss  41826  islpolN  41943  mapd0  42125  aks4d1p4  42532  aks4d1p7  42536  isprimroot  42546  linvh  42549  primrootsunit1  42550  primrootscoprmpow  42552  primrootscoprbij  42555  sticksstones3  42601  aks6d1c6lem3  42625  grpods  42647  unitscyglem2  42649  unitscyglem4  42651  unitscyglem5  42652  supinf  42695  fsuppssindlem2  43039  infdesc  43090  isnacs  43150  elmzpcl  43172  mzpindd  43192  rencldnfilem  43266  irrapxlem6  43273  pellexlem3  43277  pellexlem5  43279  elpell1qr  43293  elpell14qr  43295  elpell1234qr  43297  pellfundre  43327  pellfundge  43328  pellfundlb  43330  pellfundglb  43331  rmspecnonsq  43353  jm2.22  43441  jm2.23  43442  rpnnen3lem  43477  fnwe2lem2  43497  elmnc  43582  dgraalem  43591  dgraaub  43594  mpaalem  43598  onsucelab  43709  limnsuc  43711  sqrtcvallem1  44076  rfovcnvf1od  44449  scottelrankd  44692  nzss  44762  iccshift  45966  iooshift  45970  limcperiod  46076  sumnnodd  46078  ioodvbdlimc1lem1  46377  dvnprodlem1  46392  dvnprodlem3  46394  itgperiod  46427  stoweidlem14  46460  stoweidlem15  46461  stoweidlem16  46462  stoweidlem31  46477  stoweidlem36  46482  stoweidlem46  46492  stoweidlem48  46494  fourierdlem2  46555  fourierdlem3  46556  fourierdlem20  46573  fourierdlem25  46578  fourierdlem37  46590  fourierdlem42  46595  fourierdlem48  46600  fourierdlem51  46603  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  fourierdlem79  46631  fourierdlem81  46633  elaa2lem  46679  etransclem24  46704  etransclem26  46706  etransclem28  46708  etransclem35  46715  etransclem48  46728  salgenval  46767  salgenn0  46777  salgencl  46778  sssalgen  46781  salgenss  46782  salgenuni  46783  issalgend  46784  salgencntex  46789  subsaliuncllem  46803  sge0fodjrnlem  46862  meadjiunlem  46911  caragenel  46941  ovnlecvr  47004  ovnpnfelsup  47005  ovncvrrp  47010  ovnsubaddlem1  47016  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmv1lelem3  47039  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem4  47044  ovnhoilem1  47047  ovnlecvr2  47056  ovncvr2  47057  issmflem  47173  smflimlem2  47218  smflimlem3  47219  smflimsuplem2  47267  elsetpreimafvrab  47866  iccpart  47888  sprel  47956  prelspr  47958  sprsymrelfolem2  47965  sprsymrelf  47967  prpair  47973  paireqne  47983  prprelb  47988  prprelprb  47989  dfodd2  48124  dfeven5  48154  dfodd7  48155  fpprel  48216  clnbgrel  48316  clnbupgrel  48322  sclnbgrel  48335  vopnbgrel  48342  dfclnbgr6  48344  dfnbgr6  48345  isubgredg  48354  uhgrimisgrgric  48419  grtriprop  48429  isgrtri  48431  stgredgel  48445  stgrusgra  48447  uspgrlimlem3  48478  uspgrlim  48480  grlimgredgex  48488  grlimgrtrilem2  48490  gpgiedgdmel  48537  gpgedgel  48538  gpgnbgrvtx0  48562  gpgnbgrvtx1  48563  gpgprismgr4cycllem10  48592  1hegrlfgr  48620  assintop  48697  isassintop  48698  assintopcllaw  48700  0even  48725  2even  48727  2zrngamgm  48733  dmatALTbasel  48890  lcoval  48900  elbigo  49039  elrrx2linest2  49233  itsclc0  49259  itsclc0b  49260  itscnhlinecirc02p  49273  unilbss  49305  secval  50234  cscval  50235  cotval  50236