Theorem elrab 3644

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {crab 3412  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452

This theorem is used by:  elrab3  3645  elrabd  3646  elrabrd  3647  elrab2  3648  ralrab  3651  rexrab  3653  reurab  3658  rabsnt  4688  unimax  4904  ssintub  4925  intminss  4933  rabxfrd  5379  ssimaex  6975  weniso  7368  canth  7378  riotarab  7423  sorpsscmpl  7754  onnminsb  7817  dfom2  7883  ssnlim  7901  fnwe2lem3  8153  elsuppfng  8193  elsuppfn  8194  ressuppssdif  8209  oeeulem  8617  cofonr  8690  elpmg  8870  fineqvlem  9264  mapfienlem2  9405  supub  9458  suplub  9459  ordtypelem6  9524  ordtypelem7  9525  hartogslem1  9543  hartogs  9545  wemapsolem  9551  card2on  9555  elharval  9562  wdom2d  9581  cantnfs  9674  scottex  9940  scottexOLD  9941  scottelrankd  9955  tskwe  10038  cardid2  10041  iscard2  10064  cardmin2  10087  acni3  10133  alephsuc2  10166  kmlem1  10236  cofsmo  10354  coftr  10358  fin23lem11  10402  enfin2i  10406  fin1a2lem9  10493  fin1a2lem11  10495  axcc4  10524  axdc3lem2  10536  zorn2lem7  10587  ondomon  10654  alephval2  10664  grutsk  10914  negf1o  11753  infm3  12283  nnind  12360  peano2uz2  12794  peano5uzi  12795  dfuzi  12797  uzind  12798  uzind3  12800  eluz1  12976  uzind4  13040  nnwos  13049  eqreznegel  13068  zmin  13078  elixx1  13492  elioo2  13524  elfz1  13651  flval3  13962  serge0  14206  expge0  14248  expge1  14249  hashbclem  14604  pr2pwpr  14631  elss2prb  14640  hash2sspr  14641  wrdmap  14698  wwlktovfo  15120  shftf  15241  rlimrege0  15755  incexc2  16016  dvdsdivcl  16495  divalglem4  16575  divalgmod  16585  bitsval  16603  bezout  16725  dfgcd2  16728  lcmledvds  16783  lcmgcdlem  16790  lcmfledvds  16816  1nprm  16863  1idssfct  16864  isprm2  16866  hashdvds  16961  phisum  16977  odzval  16978  odzcllem  16979  odzdvds  16982  prmreclem2  17104  prmreclem5  17107  rami  17202  ramub1lem1  17213  ramub1lem2  17214  prmgaplem3  17240  prmgaplem4  17241  prmgaplem5  17242  prmgaplem6  17243  ismre  17769  ismri  17814  isacs  17834  isacs1i  17840  catlid  17866  catrid  17867  ismon  17917  isnat  18134  eldmcoa  18249  fncnvimaeqv  18303  lubeldm  18534  glbeldm  18547  gsumval2  18884  ismgmhm  18894  issubmgm  18900  rabsubmgmd  18902  mgmhmeql  18914  ismhm  18989  issubm  19007  issubmd  19010  mndind  19033  grplinv  19209  issubg  19345  isnsg  19374  cycsubg  19432  isgim  19485  isga  19514  elcntz  19545  elcntzsn  19548  symgfix2  19639  symgsssg  19690  symgfisg  19691  psgnunilem5  19717  odid  19761  odlem2  19762  gexid  19804  gexlem2  19805  gexdvds  19807  isslw  19831  pgpssslw  19837  pj1id  19922  oddvdssubg  20078  pgpfac1lem5  20304  ablfaclem2  20311  isirred  20658  isrnghm  20680  isrngim  20684  isrhm0  20715  isrim0  20722  rimval  20739  issubrng  20808  issubrg  20832  rgspnmin  20876  issdrg  21054  isabv  21077  islss  21218  islmhm  21311  islmim  21346  islbs  21360  isprmidl  21628  psgndiflemB  21915  elocv  21983  isobs  22035  dsmmelbas  22054  frlmelbas  22071  islinds  22124  gsumbagdiaglem  22248  rhmpsrlem2  22258  psrlidm  22278  psrridm  22279  psrass1  22280  psrcom  22284  mplsubglem  22315  mpllsslem  22316  evlsval2  22405  ismhp  22470  ismhp3  22472  mhpmulcl  22479  psdmul  22496  coe1ae0  22543  coe1mul2  22597  dmatel  22817  scmatel  22829  scmateALT  22836  symgmatr01lem  22977  pmatcoe1fsupp  23028  cpmatel  23038  chpscmat  23169  istopon  23239  fctop  23331  cctop  23333  ppttop  23334  pptbas  23335  epttop  23336  iscld  23354  clscld  23374  isnei  23430  neips  23440  neiptopnei  23459  iscn  23562  iscnp  23564  cmpsublem  23726  conncompconn  23759  2ndc1stc  23778  2ndcdisj  23784  elkgen  23864  xkoccn  23947  txdis1cn  23963  txkgen  23980  xkococnlem  23987  xkococn  23988  xkoinjcn  24015  txconn  24017  elqtop  24025  elmptrab  24155  fbssfi  24165  opnfbas  24170  elfg  24199  cfinfil  24221  csdfil  24222  supfil  24223  filssufilg  24239  uffix  24249  fixufil  24250  uffixfr  24251  elflim2  24292  fclscf  24353  flimfnfcls  24356  alexsubALTlem2  24376  alexsubALTlem4  24378  alexsubALT  24379  ptcmplem2  24381  elutop  24561  isucn  24605  iscfilu  24615  ispsmet  24632  ismet  24651  isxmet  24652  elblps  24715  elbl  24716  restmetu  24898  icccmp  25154  elcncf  25219  ishtpy  25302  isphtpy  25311  om1elbas  25362  iscfil  25595  iscau  25606  iscmet  25614  lmle  25631  rrxfsupp  25732  minveclem3  25759  minveclem4  25762  ovolshftlem1  25839  ovolscalem1  25843  ovolicc2lem3  25849  dyadmax  25928  dyadmbllem  25929  opnmbllem  25931  vitalilem2  25939  vitalilem3  25940  elcpn  26263  ig1pval3  26505  coelem  26554  quotlem  26630  elqaalem1  26651  elqaalem3  26653  aannenlem1  26664  aannenlem2  26665  dmarea  27294  jensen  27325  ftalem4  27412  efnnfsumcl  27439  efchtdvds  27495  sqff1o  27518  fsumdvdsdiaglem  27519  dvdsppwf1o  27522  dvdsflf1o  27523  dvdsflsumcom  27524  musum  27527  muinv  27529  logfac2  27553  dchrelbas  27572  lgsfle1  27642  lgsle1  27648  lgsdirprm  27667  lgsne0  27671  lgsquadlem1  27716  lgsquadlem2  27717  dchrvmasumlem1  27831  logsqvma  27878  pntleml  27947  infdesc  27976  ltsval2  28022  ltsres  28028  conway  28174  cutcuts  28176  cutbday  28179  cutsun12  28185  cutbdaybnd2  28191  cutbdaylt  28193  bday1  28209  cutlt  28327  precsexlem8  28609  precsexlem9  28610  precsexlem11  28612  oncutlt  28659  noseqinds  28688  peano5uzs  28799  uzsind  28800  tgellng  29025  mircgr  29138  mirbtwn  29139  elplng  29267  iseqlg  29421  ttgelitv  29469  upgrle  29677  upgrbi  29680  umgredg2  29687  umgrbi  29688  edgupgr  29721  edgumgr  29722  upgredg  29724  numedglnl  29731  edgusgr  29750  usgruspgrb  29773  usgredg2ALT  29783  ushgredgedg  29819  ushgredgedgloop  29821  usgrexmplef  29849  upgrreslem  29894  umgrreslem  29895  upgrres1  29903  nbgrel  29930  nbupgrel  29935  nbumgrvtx  29936  nbusgreledg  29943  nbgrnself  29949  uvtxusgrel  29993  vtxdgoddnumeven  30143  rgrusgrprc  30179  lfgrwlkprop  30279  iswwlks  30434  iswwlksn  30436  wwlksnextsurj  30498  rusgrnumwwlkslem  30570  rusgrnumwwlks  30575  isclwwlk  30584  clwwlknscsh  30662  eleclclwwlkn  30676  clwlknf1oclwwlkn  30684  clwwlkvbij  30713  eupth2lems  30848  konigsberglem4  30865  fusgreg2wsplem  30943  2clwwlkel  30959  extwwlkfabel  30963  clwwlknonclwlknonf1o  30972  dlwwlknondlwlknonf1o  30975  numclwwlk2lem1  30986  numclwlk2lem2f  30987  numclwlk2lem2f1o  30989  grpoidinv2  31126  grpoinv  31136  isssp  31335  islno  31364  isblo  31393  ishmo  31422  ubthlem1  31481  ubthlem2  31482  htthlem  31528  ocel  31892  shsval2i  31998  ococin  32019  chsupsn  32024  eleigvec  32568  cnlnadjlem5  32682  shatomistici  32972  hatomistici  32973  dmrab  33144  nnindf  33461  indf1ofs  33483  ismnt  33594  pwrssmgc  33611  tocycf  33728  tocyc01  33729  trsp2cyc  33734  cycpmco2f1  33735  cycpmco2rn  33736  cycpmco2lem2  33738  cycpmco2lem3  33739  cycpmco2lem5  33741  cycpmco2lem6  33742  cycpmco2lem7  33743  cycpmconjv  33753  tocyccntz  33755  cyc3evpm  33761  cycpmgcl  33764  cyc3conja  33768  isfxp  33779  fxpgaeq  33780  elrgspnsubrun  33860  rlocisunit  33887  fldgensdrg  33926  nsgmgclem  34012  nsgmgc  34013  nsgqusf1olem2  34015  ismxidl  34037  ssmxidl  34049  isrprm  34099  1arithufdlem3  34128  1arithufdlem4  34129  1arithufd  34130  mplvrpmga  34227  mplvrpmmhm  34228  fedgmullem2  34312  ply1annnr  34385  minplyann  34391  minplyirred  34393  constrsuc  34420  zarclsiin  34553  zart0  34561  rhmpreimacnlem  34566  ordtconnlem1  34606  sigagenval  34823  ldsysgenld  34843  ldgenpisyslem1  34846  ldgenpisyslem2  34847  ldgenpisys  34849  ddemeas  34919  ismbfm  34934  imambfm  34944  dya2iocuni  34965  oms0  34979  omssubadd  34982  elcarsg  34987  issibf  35015  sitgfval  35023  oddpwdc  35036  eulerpartlemgh  35060  eulerpartlemgs2  35062  dstfrvel  35156  ballotlemfc0  35175  ballotlemfcc  35176  ballotlemiex  35184  ballotlemfrcn0  35212  ballotlemirc  35214  ballotlem7  35218  reprsum  35292  reprsuc  35294  reprpmtf1o  35305  reprdifc  35306  fnrelpredd  35776  fineqvnttrclselem2  35850  connpconn  36090  iscvm  36114  cvmsi  36120  cvmsval  36121  cvmliftmolem2  36137  cvmliftiota  36156  snmlval  36186  satfv1lem  36217  fmlafvel  36240  fmla1  36242  fmlaomn0  36245  satfv0fvfmla0  36268  sategoelfvb  36274  elmpst  36391  lineelsb2  37009  linerflx1  37010  fwddifval  37023  fwddifnval  37024  rankeq1o  37028  finminlem  37202  fneint  37232  fnessref  37241  topmeet  37248  topjoin  37249  neifg  37255  weiunlem  37347  weiunfrlem  37348  weiunse  37352  regsfromregtco  37422  relowlssretop  38395  fin2solem  38638  fin2so  38639  poimirlem4  38651  poimirlem25  38672  poimirlem26  38673  poimirlem27  38674  poimirlem31  38678  poimirlem32  38679  opnmbllem0  38683  mblfinlem2  38685  itg2gt0cn  38702  indexa  38776  nninfnub  38794  istotbnd  38812  sstotbnd2  38817  isbnd  38823  isrngohom  39008  isrngoiso  39021  isidl  39057  ispridl  39077  ismaxidl  39083  prnc  39110  isfldidl  39111  islshp  40145  lssats  40178  islfl  40226  isat  40452  atlatmstc  40485  islln  40672  islpln  40696  islvol  40739  linepsubN  40918  elpmap  40924  pmapsub  40934  elpadd  40965  paddvaln0N  40967  islhp  41162  isldil  41276  isltrn  41285  isdilN  41320  istrnN  41323  diaval  42198  diaelval  42199  diaeldm  42202  diaelrnN  42211  cdlemm10N  42284  docaclN  42290  dibglbN  42332  dicval  42342  dicfnN  42349  dicvalrelN  42351  dihglblem2aN  42459  dihglblem2N  42460  dihglblem3N  42461  dih1dimatlem  42495  dihglb2  42508  dochvalr  42523  doch2val2  42530  dochocss  42532  islpolN  42649  mapd0  42831  aks4d1p4  43238  aks4d1p7  43242  isprimroot  43252  linvh  43255  primrootsunit1  43256  primrootscoprmpow  43258  primrootscoprbij  43261  sticksstones3  43307  aks6d1c6lem3  43331  grpods  43353  unitscyglem2  43355  unitscyglem4  43357  unitscyglem5  43358  supinf  43402  fsuppssindlem2  43729  isnacs  43824  elmzpcl  43846  mzpindd  43866  rencldnfilem  43936  irrapxlem6  43943  pellexlem3  43947  pellexlem5  43949  elpell1qr  43963  elpell14qr  43965  elpell1234qr  43967  pellfundre  43997  pellfundge  43998  pellfundlb  44000  pellfundglb  44001  rmspecnonsq  44023  jm2.22  44111  jm2.23  44112  rpnnen3lem  44147  elmnc  44247  dgraalem  44256  dgraaub  44259  mpaalem  44263  onsucelab  44374  limnsuc  44376  sqrtcvallem1  44740  rfovcnvf1od  45113  nzss  45410  iccshift  46638  iooshift  46642  limcperiod  46748  sumnnodd  46750  ioodvbdlimc1lem1  47049  dvnprodlem1  47064  dvnprodlem3  47066  itgperiod  47099  stoweidlem14  47132  stoweidlem15  47133  stoweidlem16  47134  stoweidlem31  47149  stoweidlem36  47154  stoweidlem46  47164  stoweidlem48  47166  fourierdlem2  47227  fourierdlem3  47228  fourierdlem20  47245  fourierdlem25  47250  fourierdlem37  47262  fourierdlem42  47267  fourierdlem48  47272  fourierdlem51  47275  fourierdlem63  47287  fourierdlem64  47288  fourierdlem65  47289  fourierdlem79  47303  fourierdlem81  47305  elaa2lem  47351  etransclem24  47376  etransclem26  47378  etransclem28  47380  etransclem35  47387  etransclem48  47400  salgenval  47439  salgenn0  47449  salgencl  47450  sssalgen  47453  salgenss  47454  salgenuni  47455  issalgend  47456  salgencntex  47461  subsaliuncllem  47475  sge0fodjrnlem  47534  meadjiunlem  47583  caragenel  47613  ovnlecvr  47676  ovnpnfelsup  47677  ovncvrrp  47682  ovnsubaddlem1  47688  hoidmv1lelem1  47709  hoidmv1lelem2  47710  hoidmv1lelem3  47711  hoidmvlelem1  47713  hoidmvlelem2  47714  hoidmvlelem4  47716  ovnhoilem1  47719  ovnlecvr2  47728  ovncvr2  47729  issmflem  47845  smflimlem2  47890  smflimlem3  47891  smflimsuplem2  47939  elsetpreimafvrab  48584  iccpart  48606  sprel  48674  prelspr  48676  sprsymrelfolem2  48683  sprsymrelf  48685  prpair  48691  paireqne  48701  prprelb  48706  prprelprb  48707  dfodd2  48842  dfeven5  48872  dfodd7  48873  fpprel  48934  clnbgrel  49034  clnbupgrel  49040  sclnbgrel  49053  vopnbgrel  49060  dfclnbgr6  49062  dfnbgr6  49063  isubgredg  49072  uhgrimisgrgric  49137  grtriprop  49147  isgrtri  49149  stgredgel  49163  stgrusgra  49165  uspgrlimlem3  49196  uspgrlim  49198  grlimgredgex  49206  grlimgrtrilem2  49208  gpgiedgdmel  49255  gpgedgel  49256  gpgnbgrvtx0  49280  gpgnbgrvtx1  49281  gpgprismgr4cycllem10  49310  1hegrlfgr  49338  assintop  49414  isassintop  49415  assintopcllaw  49417  0even  49442  2even  49444  2zrngamgm  49450  dmatALTbasel  49622  lcoval  49632  elbigo  49771  elrrx2linest2  49965  itsclc0  49991  itsclc0b  49992  itscnhlinecirc02p  50005  unilbss  50037  secval  51023  cscval  51024  cotval  51025  dvsec  51039  dvcsc  51040  dvcot  51041