Theorem elrab 3676

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  {crab 3424  Vcvv 3466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468

This theorem is referenced by:  elrab3  3677  elrabd  3678  elrab2  3679  ralrab  3682  rexrab  3685  reurab  3690  rabsnt  4728  unimax  4939  ssintub  4961  intminss  4969  rabxfrd  5406  ssimaex  6967  weniso  7344  canth  7355  riotarab  7401  sorpsscmpl  7718  onnminsb  7781  dfom2  7851  ssnlim  7869  elsuppfng  8150  elsuppfn  8151  ressuppssdif  8165  oeeulem  8597  cofonr  8670  elpmg  8834  fineqvlem  9259  mapfienlem2  9398  supub  9451  suplub  9452  ordtypelem6  9515  ordtypelem7  9516  hartogslem1  9534  hartogs  9536  wemapsolem  9542  card2on  9546  elharval  9553  wdom2d  9572  cantnfs  9658  scottex  9877  tskwe  9942  cardid2  9945  iscard2  9968  cardmin2  9991  acni3  10039  alephsuc2  10072  kmlem1  10142  cofsmo  10261  coftr  10265  fin23lem11  10309  enfin2i  10313  fin1a2lem9  10400  fin1a2lem11  10402  axcc4  10431  axdc3lem2  10443  zorn2lem7  10494  ondomon  10555  alephval2  10564  grutsk  10814  negf1o  11642  infm3  12171  nnind  12228  peano2uz2  12648  peano5uzi  12649  dfuzi  12651  uzind  12652  uzind3  12654  eluz1  12824  uzind4  12888  nnwos  12897  eqreznegel  12916  zmin  12926  elixx1  13331  elioo2  13363  elfz1  13487  flval3  13778  serge0  14020  expge0  14062  expge1  14063  hashbclem  14409  pr2pwpr  14438  elss2prb  14446  hash2sspr  14447  wrdmap  14494  wwlktovfo  14907  shftf  15024  rlimrege0  15521  incexc2  15782  dvdsdivcl  16258  divalglem4  16338  divalgmod  16348  bitsval  16364  bezout  16484  dfgcd2  16487  lcmledvds  16535  lcmgcdlem  16542  lcmfledvds  16568  1nprm  16615  1idssfct  16616  isprm2  16618  hashdvds  16709  phisum  16724  odzval  16725  odzcllem  16726  odzdvds  16729  prmreclem2  16851  prmreclem5  16854  rami  16949  ramub1lem1  16960  ramub1lem2  16961  prmgaplem3  16987  prmgaplem4  16988  prmgaplem5  16989  prmgaplem6  16990  ismre  17535  ismri  17576  isacs  17596  isacs1i  17602  catlid  17628  catrid  17629  ismon  17681  isnat  17902  eldmcoa  18019  fncnvimaeqv  18075  lubeldm  18310  glbeldm  18323  gsumval2  18611  ismgmhm  18621  issubmgm  18627  rabsubmgmd  18629  mgmhmeql  18641  ismhm  18707  issubm  18720  issubmd  18723  mndind  18745  grplinv  18911  issubg  19045  isnsg  19074  cycsubg  19126  isgim  19179  isga  19199  elcntz  19230  elcntzsn  19233  symgfix2  19328  symgsssg  19379  symgfisg  19380  psgnunilem5  19406  odid  19450  odlem2  19451  gexid  19493  gexlem2  19494  gexdvds  19496  isslw  19520  pgpssslw  19526  pj1id  19611  oddvdssubg  19767  pgpfac1lem5  19993  ablfaclem2  20000  isirred  20313  isrnghm  20335  isrngim  20339  isrim0OLD  20375  isrim0  20377  issubrng  20439  issubrg  20465  issdrg  20631  isabv  20654  islss  20773  islmhm  20867  islmim  20902  islbs  20916  psgndiflemB  21463  elocv  21531  isobs  21585  dsmmelbas  21604  frlmelbas  21621  islinds  21674  gsumbagdiaglemOLD  21802  gsumbagdiaglem  21805  psrmulcllem  21818  psrlidm  21835  psrridm  21836  psrass1  21837  psrcom  21841  mplsubglem  21870  mpllsslem  21871  evlsval2  21962  ismhp  21994  ismhp3  21996  mhpmulcl  22002  coe1ae0  22060  coe1mul2  22112  dmatel  22319  scmatel  22331  scmateALT  22338  symgmatr01lem  22479  pmatcoe1fsupp  22527  cpmatel  22537  chpscmat  22668  istopon  22738  fctop  22831  cctop  22833  ppttop  22834  pptbas  22835  epttop  22836  iscld  22855  clscld  22875  isnei  22931  neips  22941  neiptopnei  22960  iscn  23063  iscnp  23065  cmpsublem  23227  conncompconn  23260  2ndc1stc  23279  2ndcdisj  23284  elkgen  23364  xkoccn  23447  txdis1cn  23463  txkgen  23480  xkococnlem  23487  xkococn  23488  xkoinjcn  23515  txconn  23517  elqtop  23525  elmptrab  23655  fbssfi  23665  opnfbas  23670  elfg  23699  cfinfil  23721  csdfil  23722  supfil  23723  filssufilg  23739  uffix  23749  fixufil  23750  uffixfr  23751  elflim2  23792  fclscf  23853  flimfnfcls  23856  alexsubALTlem2  23876  alexsubALTlem4  23878  alexsubALT  23879  ptcmplem2  23881  elutop  24062  isucn  24107  iscfilu  24117  ispsmet  24134  ismet  24153  isxmet  24154  elblps  24217  elbl  24218  restmetu  24403  icccmp  24665  elcncf  24733  ishtpy  24822  isphtpy  24831  om1elbas  24883  iscfil  25117  iscau  25128  iscmet  25136  lmle  25153  rrxfsupp  25254  minveclem3  25281  minveclem4  25284  ovolshftlem1  25362  ovolscalem1  25366  ovolicc2lem3  25372  dyadmax  25451  dyadmbllem  25452  opnmbllem  25454  vitalilem2  25462  vitalilem3  25463  elcpn  25788  ig1pval3  26034  coelem  26082  quotlem  26156  elqaalem1  26175  elqaalem3  26177  aannenlem1  26184  aannenlem2  26185  dmarea  26808  jensen  26840  ftalem4  26927  efnnfsumcl  26954  efchtdvds  27010  sqff1o  27033  fsumdvdsdiaglem  27034  dvdsppwf1o  27037  dvdsflf1o  27038  dvdsflsumcom  27039  musum  27042  muinv  27044  logfac2  27069  dchrelbas  27088  lgsfle1  27158  lgsle1  27164  lgsdirprm  27183  lgsne0  27187  lgsquadlem1  27232  lgsquadlem2  27233  dchrvmasumlem1  27347  logsqvma  27394  pntleml  27463  sltval2  27508  sltres  27514  conway  27651  scutcut  27653  scutbday  27656  scutun12  27662  scutbdaybnd2  27668  scutbdaylt  27670  bday1s  27683  cutlt  27771  precsexlem8  28031  precsexlem9  28032  precsexlem11  28034  noseqinds  28085  tgellng  28276  mircgr  28380  mirbtwn  28381  iseqlg  28590  ttgelitv  28612  upgrle  28822  upgrbi  28825  umgredg2  28832  umgrbi  28833  edgupgr  28866  edgumgr  28867  upgredg  28869  numedglnl  28876  edgusgr  28892  usgruspgrb  28913  usgredg2ALT  28922  ushgredgedg  28958  ushgredgedgloop  28960  usgrexmplef  28988  upgrreslem  29033  umgrreslem  29034  upgrres1  29042  nbgrel  29069  nbupgrel  29074  nbumgrvtx  29075  nbusgreledg  29082  nbgrnself  29088  uvtxusgrel  29132  vtxdgoddnumeven  29282  rgrusgrprc  29318  lfgrwlkprop  29416  iswwlks  29562  iswwlksn  29564  wwlksnextsurj  29626  rusgrnumwwlkslem  29695  rusgrnumwwlks  29700  isclwwlk  29709  clwwlknscsh  29787  eleclclwwlkn  29801  clwlknf1oclwwlkn  29809  clwwlkvbij  29838  eupth2lems  29963  konigsberglem4  29980  fusgreg2wsplem  30058  2clwwlkel  30074  extwwlkfabel  30078  clwwlknonclwlknonf1o  30087  dlwwlknondlwlknonf1o  30090  numclwwlk2lem1  30101  numclwlk2lem2f  30102  numclwlk2lem2f1o  30104  grpoidinv2  30240  grpoinv  30250  isssp  30449  islno  30478  isblo  30507  ishmo  30536  ubthlem1  30595  ubthlem2  30596  htthlem  30642  ocel  31006  shsval2i  31112  ococin  31133  chsupsn  31138  eleigvec  31682  cnlnadjlem5  31796  shatomistici  32086  hatomistici  32087  dmrab  32209  nnindf  32495  ismnt  32623  pwrssmgc  32640  tocycf  32747  tocyc01  32748  trsp2cyc  32753  cycpmco2f1  32754  cycpmco2rn  32755  cycpmco2lem2  32757  cycpmco2lem3  32758  cycpmco2lem5  32760  cycpmco2lem6  32761  cycpmco2lem7  32762  cycpmconjv  32772  tocyccntz  32774  cyc3evpm  32780  cycpmgcl  32783  cycpmconjslem2  32785  cyc3conja  32787  fldgensdrg  32873  nsgmgclem  32994  nsgmgc  32995  nsgqusf1olem2  32997  isprmidl  33028  ismxidl  33050  ssmxidl  33062  isrprm  33106  fedgmullem2  33197  ply1annnr  33247  minplyirred  33253  zarclsiin  33343  zart0  33351  rhmpreimacnlem  33356  ordtconnlem1  33396  indf1ofs  33516  sigagenval  33630  ldsysgenld  33650  ldgenpisyslem1  33653  ldgenpisyslem2  33654  ldgenpisys  33656  ddemeas  33726  ismbfm  33741  imambfm  33753  dya2iocuni  33774  oms0  33788  omssubadd  33791  elcarsg  33796  issibf  33824  sitgfval  33832  oddpwdc  33845  eulerpartlemgh  33869  eulerpartlemgs2  33871  dstfrvel  33964  ballotlemfc0  33983  ballotlemfcc  33984  ballotlemiex  33992  ballotlemfrcn0  34020  ballotlemirc  34022  ballotlem7  34026  reprsum  34116  reprsuc  34118  reprpmtf1o  34129  reprdifc  34130  fnrelpredd  34583  connpconn  34717  iscvm  34741  cvmsi  34747  cvmsval  34748  cvmliftmolem2  34764  cvmliftiota  34783  snmlval  34813  satfv1lem  34844  fmlafvel  34867  fmla1  34869  fmlaomn0  34872  satfv0fvfmla0  34895  sategoelfvb  34901  elmpst  35018  lineelsb2  35616  linerflx1  35617  fwddifval  35630  fwddifnval  35631  rankeq1o  35639  finminlem  35694  fneint  35724  fnessref  35733  topmeet  35740  topjoin  35741  neifg  35747  relowlssretop  36735  fin2solem  36968  fin2so  36969  poimirlem4  36986  poimirlem25  37007  poimirlem26  37008  poimirlem27  37009  poimirlem31  37013  poimirlem32  37014  opnmbllem0  37018  mblfinlem2  37020  itg2gt0cn  37037  indexa  37095  nninfnub  37113  istotbnd  37131  sstotbnd2  37136  isbnd  37142  isrngohom  37327  isrngoiso  37340  isidl  37376  ispridl  37396  ismaxidl  37402  prnc  37429  isfldidl  37430  islshp  38343  lssats  38376  islfl  38424  isat  38650  atlatmstc  38683  islln  38871  islpln  38895  islvol  38938  linepsubN  39117  elpmap  39123  pmapsub  39133  elpadd  39164  paddvaln0N  39166  islhp  39361  isldil  39475  isltrn  39484  isdilN  39519  istrnN  39522  diaval  40397  diaelval  40398  diaeldm  40401  diaelrnN  40410  cdlemm10N  40483  docaclN  40489  dibglbN  40531  dicval  40541  dicfnN  40548  dicvalrelN  40550  dihglblem2aN  40658  dihglblem2N  40659  dihglblem3N  40660  dih1dimatlem  40694  dihglb2  40707  dochvalr  40722  doch2val2  40729  dochocss  40731  islpolN  40848  mapd0  41030  aks4d1p4  41441  aks4d1p7  41445  sticksstones3  41461  rhmmpllem2  41615  rhmcomulmpl  41617  fsuppssindlem2  41657  infdesc  41899  isnacs  41956  elmzpcl  41978  mzpindd  41998  rencldnfilem  42072  irrapxlem6  42079  pellexlem3  42083  pellexlem5  42085  elpell1qr  42099  elpell14qr  42101  elpell1234qr  42103  pellfundre  42133  pellfundge  42134  pellfundlb  42136  pellfundglb  42137  rmspecnonsq  42159  jm2.22  42248  jm2.23  42249  rpnnen3lem  42284  fnwe2lem2  42307  elmnc  42392  dgraalem  42401  dgraaub  42404  mpaalem  42408  rgspnmin  42427  onsucelab  42527  limnsuc  42529  sqrtcvallem1  42896  rfovcnvf1od  43269  scottelrankd  43520  nzss  43590  iccshift  44741  iooshift  44745  limcperiod  44854  sumnnodd  44856  ioodvbdlimc1lem1  45157  dvnprodlem1  45172  dvnprodlem3  45174  itgperiod  45207  stoweidlem14  45240  stoweidlem15  45241  stoweidlem16  45242  stoweidlem31  45257  stoweidlem36  45262  stoweidlem46  45272  stoweidlem48  45274  fourierdlem2  45335  fourierdlem3  45336  fourierdlem20  45353  fourierdlem25  45358  fourierdlem37  45370  fourierdlem42  45375  fourierdlem48  45380  fourierdlem51  45383  fourierdlem63  45395  fourierdlem64  45396  fourierdlem65  45397  fourierdlem79  45411  fourierdlem81  45413  elaa2lem  45459  etransclem24  45484  etransclem26  45486  etransclem28  45488  etransclem35  45495  etransclem48  45508  salgenval  45547  salgenn0  45557  salgencl  45558  sssalgen  45561  salgenss  45562  salgenuni  45563  issalgend  45564  salgencntex  45569  subsaliuncllem  45583  sge0fodjrnlem  45642  meadjiunlem  45691  caragenel  45721  ovnlecvr  45784  ovnpnfelsup  45785  ovncvrrp  45790  ovnsubaddlem1  45796  hoidmv1lelem1  45817  hoidmv1lelem2  45818  hoidmv1lelem3  45819  hoidmvlelem1  45821  hoidmvlelem2  45822  hoidmvlelem4  45824  ovnhoilem1  45827  ovnlecvr2  45836  ovncvr2  45837  issmflem  45953  smflimlem2  45998  smflimlem3  45999  smflimsuplem2  46047  elsetpreimafvrab  46572  iccpart  46594  sprel  46662  prelspr  46664  sprsymrelfolem2  46671  sprsymrelf  46673  prpair  46679  paireqne  46689  prprelb  46694  prprelprb  46695  dfodd2  46814  dfeven5  46844  dfodd7  46845  fpprel  46906  1hegrlfgr  47020  assintop  47097  isassintop  47098  assintopcllaw  47100  0even  47125  2even  47127  2zrngamgm  47133  dmatALTbasel  47296  lcoval  47306  elbigo  47450  elrrx2linest2  47644  itsclc0  47670  itsclc0b  47671  itscnhlinecirc02p  47684  unilbss  47714  secval  48004  cscval  48005  cotval  48006