Theorem elrab 3645

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 3634	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓)))
9	1, 3, 8	pm5.21nii 381	1 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜑} ↔ (𝐴 ∈ 𝐵 ∧ 𝜓))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

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

This theorem is used by:  elrab3  3646  elrabd  3647  elrabrd  3648  elrab2  3649  ralrab  3652  rexrab  3654  reurab  3659  rabsnt  4692  unimax  4905  ssintub  4926  intminss  4934  rabxfrd  5382  ssimaex  6963  weniso  7357  canth  7367  riotarab  7412  sorpsscmpl  7735  onnminsb  7798  dfom2  7864  ssnlim  7882  elsuppfng  8167  elsuppfn  8168  ressuppssdif  8183  oeeulem  8589  cofonr  8662  elpmg  8842  fineqvlem  9236  mapfienlem2  9376  supub  9429  suplub  9430  ordtypelem6  9495  ordtypelem7  9496  hartogslem1  9514  hartogs  9516  wemapsolem  9522  card2on  9526  elharval  9533  wdom2d  9552  cantnfs  9645  scottex  9872  scottexOLD  9873  scottelrankd  9887  tskwe  9955  cardid2  9958  iscard2  9981  cardmin2  10004  acni3  10050  alephsuc2  10083  kmlem1  10153  cofsmo  10271  coftr  10275  fin23lem11  10319  enfin2i  10323  fin1a2lem9  10410  fin1a2lem11  10412  axcc4  10441  axdc3lem2  10453  zorn2lem7  10504  ondomon  10571  alephval2  10581  grutsk  10831  negf1o  11668  infm3  12198  nnind  12275  peano2uz2  12709  peano5uzi  12710  dfuzi  12712  uzind  12713  uzind3  12715  eluz1  12891  uzind4  12955  nnwos  12964  eqreznegel  12983  zmin  12993  elixx1  13407  elioo2  13439  elfz1  13566  flval3  13876  serge0  14120  expge0  14162  expge1  14163  hashbclem  14517  pr2pwpr  14544  elss2prb  14553  hash2sspr  14554  wrdmap  14611  wwlktovfo  15031  shftf  15152  rlimrege0  15666  incexc2  15927  dvdsdivcl  16406  divalglem4  16486  divalgmod  16496  bitsval  16514  bezout  16633  dfgcd2  16636  lcmledvds  16689  lcmgcdlem  16696  lcmfledvds  16722  1nprm  16769  1idssfct  16770  isprm2  16772  hashdvds  16866  phisum  16882  odzval  16883  odzcllem  16884  odzdvds  16887  prmreclem2  17009  prmreclem5  17012  rami  17107  ramub1lem1  17118  ramub1lem2  17119  prmgaplem3  17145  prmgaplem4  17146  prmgaplem5  17147  prmgaplem6  17148  ismre  17674  ismri  17719  isacs  17739  isacs1i  17745  catlid  17771  catrid  17772  ismon  17822  isnat  18039  eldmcoa  18154  fncnvimaeqv  18208  lubeldm  18439  glbeldm  18452  gsumval2  18788  ismgmhm  18798  issubmgm  18804  rabsubmgmd  18806  mgmhmeql  18818  ismhm  18893  issubm  18911  issubmd  18914  mndind  18937  grplinv  19113  issubg  19249  isnsg  19278  cycsubg  19336  isgim  19389  isga  19418  elcntz  19449  elcntzsn  19452  symgfix2  19543  symgsssg  19594  symgfisg  19595  psgnunilem5  19621  odid  19665  odlem2  19666  gexid  19708  gexlem2  19709  gexdvds  19711  isslw  19735  pgpssslw  19741  pj1id  19826  oddvdssubg  19982  pgpfac1lem5  20208  ablfaclem2  20215  isirred  20560  isrnghm  20582  isrngim  20586  isrhm0  20617  isrim0  20624  rimval  20641  issubrng  20709  issubrg  20733  rgspnmin  20777  issdrg  20954  isabv  20977  islss  21118  islmhm  21211  islmim  21246  islbs  21260  isprmidl  21526  psgndiflemB  21813  elocv  21881  isobs  21933  dsmmelbas  21952  frlmelbas  21969  islinds  22022  gsumbagdiaglem  22146  rhmpsrlem2  22156  psrlidm  22176  psrridm  22177  psrass1  22178  psrcom  22182  mplsubglem  22213  mpllsslem  22214  evlsval2  22303  ismhp  22368  ismhp3  22370  mhpmulcl  22377  psdmul  22394  coe1ae0  22441  coe1mul2  22495  dmatel  22715  scmatel  22727  scmateALT  22734  symgmatr01lem  22875  pmatcoe1fsupp  22926  cpmatel  22936  chpscmat  23067  istopon  23137  fctop  23229  cctop  23231  ppttop  23232  pptbas  23233  epttop  23234  iscld  23252  clscld  23272  isnei  23328  neips  23338  neiptopnei  23357  iscn  23460  iscnp  23462  cmpsublem  23624  conncompconn  23657  2ndc1stc  23676  2ndcdisj  23682  elkgen  23762  xkoccn  23845  txdis1cn  23861  txkgen  23878  xkococnlem  23885  xkococn  23886  xkoinjcn  23913  txconn  23915  elqtop  23923  elmptrab  24053  fbssfi  24063  opnfbas  24068  elfg  24097  cfinfil  24119  csdfil  24120  supfil  24121  filssufilg  24137  uffix  24147  fixufil  24148  uffixfr  24149  elflim2  24190  fclscf  24251  flimfnfcls  24254  alexsubALTlem2  24274  alexsubALTlem4  24276  alexsubALT  24277  ptcmplem2  24279  elutop  24459  isucn  24503  iscfilu  24513  ispsmet  24530  ismet  24549  isxmet  24550  elblps  24613  elbl  24614  restmetu  24796  icccmp  25052  elcncf  25117  ishtpy  25200  isphtpy  25209  om1elbas  25260  iscfil  25493  iscau  25504  iscmet  25512  lmle  25529  rrxfsupp  25630  minveclem3  25657  minveclem4  25660  ovolshftlem1  25737  ovolscalem1  25741  ovolicc2lem3  25747  dyadmax  25826  dyadmbllem  25827  opnmbllem  25829  vitalilem2  25837  vitalilem3  25838  elcpn  26161  ig1pval3  26403  coelem  26452  quotlem  26530  elqaalem1  26551  elqaalem3  26553  aannenlem1  26564  aannenlem2  26565  dmarea  27194  jensen  27225  ftalem4  27312  efnnfsumcl  27339  efchtdvds  27395  sqff1o  27418  fsumdvdsdiaglem  27419  dvdsppwf1o  27422  dvdsflf1o  27423  dvdsflsumcom  27424  musum  27427  muinv  27429  logfac2  27453  dchrelbas  27472  lgsfle1  27542  lgsle1  27548  lgsdirprm  27567  lgsne0  27571  lgsquadlem1  27616  lgsquadlem2  27617  dchrvmasumlem1  27731  logsqvma  27778  pntleml  27847  ltsval2  27892  ltsres  27898  conway  28044  cutcuts  28046  cutbday  28049  cutsun12  28055  cutbdaybnd2  28061  cutbdaylt  28063  bday1  28079  cutlt  28197  precsexlem8  28479  precsexlem9  28480  precsexlem11  28482  oncutlt  28529  noseqinds  28558  peano5uzs  28669  uzsind  28670  tgellng  28895  mircgr  29008  mirbtwn  29009  elplng  29137  iseqlg  29291  ttgelitv  29339  upgrle  29547  upgrbi  29550  umgredg2  29557  umgrbi  29558  edgupgr  29591  edgumgr  29592  upgredg  29594  numedglnl  29601  edgusgr  29620  usgruspgrb  29643  usgredg2ALT  29653  ushgredgedg  29689  ushgredgedgloop  29691  usgrexmplef  29719  upgrreslem  29764  umgrreslem  29765  upgrres1  29773  nbgrel  29800  nbupgrel  29805  nbumgrvtx  29806  nbusgreledg  29813  nbgrnself  29819  uvtxusgrel  29863  vtxdgoddnumeven  30013  rgrusgrprc  30049  lfgrwlkprop  30149  iswwlks  30304  iswwlksn  30306  wwlksnextsurj  30368  rusgrnumwwlkslem  30440  rusgrnumwwlks  30445  isclwwlk  30454  clwwlknscsh  30532  eleclclwwlkn  30546  clwlknf1oclwwlkn  30554  clwwlkvbij  30583  eupth2lems  30718  konigsberglem4  30735  fusgreg2wsplem  30813  2clwwlkel  30829  extwwlkfabel  30833  clwwlknonclwlknonf1o  30842  dlwwlknondlwlknonf1o  30845  numclwwlk2lem1  30856  numclwlk2lem2f  30857  numclwlk2lem2f1o  30859  grpoidinv2  30996  grpoinv  31006  isssp  31205  islno  31234  isblo  31263  ishmo  31292  ubthlem1  31351  ubthlem2  31352  htthlem  31398  ocel  31762  shsval2i  31868  ococin  31889  chsupsn  31894  eleigvec  32438  cnlnadjlem5  32552  shatomistici  32842  hatomistici  32843  dmrab  32972  nnindf  33290  indf1ofs  33312  ismnt  33423  pwrssmgc  33440  tocycf  33557  tocyc01  33558  trsp2cyc  33563  cycpmco2f1  33564  cycpmco2rn  33565  cycpmco2lem2  33567  cycpmco2lem3  33568  cycpmco2lem5  33570  cycpmco2lem6  33571  cycpmco2lem7  33572  cycpmconjv  33582  tocyccntz  33584  cyc3evpm  33590  cycpmgcl  33593  cyc3conja  33597  isfxp  33608  fxpgaeq  33609  elrgspnsubrun  33689  rlocisunit  33716  fldgensdrg  33755  nsgmgclem  33840  nsgmgc  33841  nsgqusf1olem2  33843  ismxidl  33865  ssmxidl  33877  isrprm  33927  1arithufdlem3  33956  1arithufdlem4  33957  1arithufd  33958  mplvrpmga  34055  mplvrpmmhm  34056  fedgmullem2  34140  ply1annnr  34213  minplyann  34219  minplyirred  34221  constrsuc  34248  zarclsiin  34381  zart0  34389  rhmpreimacnlem  34394  ordtconnlem1  34434  sigagenval  34651  ldsysgenld  34671  ldgenpisyslem1  34674  ldgenpisyslem2  34675  ldgenpisys  34677  ddemeas  34747  ismbfm  34762  imambfm  34773  dya2iocuni  34794  oms0  34808  omssubadd  34811  elcarsg  34816  issibf  34844  sitgfval  34852  oddpwdc  34865  eulerpartlemgh  34889  eulerpartlemgs2  34891  dstfrvel  34985  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemiex  35013  ballotlemfrcn0  35041  ballotlemirc  35043  ballotlem7  35047  reprsum  35121  reprsuc  35123  reprpmtf1o  35134  reprdifc  35135  fnrelpredd  35596  fineqvnttrclselem2  35648  connpconn  35814  iscvm  35838  cvmsi  35844  cvmsval  35845  cvmliftmolem2  35861  cvmliftiota  35880  snmlval  35910  satfv1lem  35941  fmlafvel  35964  fmla1  35966  fmlaomn0  35969  satfv0fvfmla0  35992  sategoelfvb  35998  elmpst  36115  lineelsb2  36728  linerflx1  36729  fwddifval  36742  fwddifnval  36743  rankeq1o  36751  finminlem  36937  fneint  36967  fnessref  36976  topmeet  36983  topjoin  36984  neifg  36990  weiunlem  37082  weiunfrlem  37083  weiunse  37087  regsfromregtco  37157  relowlssretop  38117  fin2solem  38360  fin2so  38361  poimirlem4  38373  poimirlem25  38394  poimirlem26  38395  poimirlem27  38396  poimirlem31  38400  poimirlem32  38401  opnmbllem0  38405  mblfinlem2  38407  itg2gt0cn  38424  indexa  38483  nninfnub  38501  istotbnd  38519  sstotbnd2  38524  isbnd  38530  isrngohom  38715  isrngoiso  38728  isidl  38764  ispridl  38784  ismaxidl  38790  prnc  38817  isfldidl  38818  islshp  39852  lssats  39885  islfl  39933  isat  40159  atlatmstc  40192  islln  40379  islpln  40403  islvol  40446  linepsubN  40625  elpmap  40631  pmapsub  40641  elpadd  40672  paddvaln0N  40674  islhp  40869  isldil  40983  isltrn  40992  isdilN  41027  istrnN  41030  diaval  41905  diaelval  41906  diaeldm  41909  diaelrnN  41918  cdlemm10N  41991  docaclN  41997  dibglbN  42039  dicval  42049  dicfnN  42056  dicvalrelN  42058  dihglblem2aN  42166  dihglblem2N  42167  dihglblem3N  42168  dih1dimatlem  42202  dihglb2  42215  dochvalr  42230  doch2val2  42237  dochocss  42239  islpolN  42356  mapd0  42538  aks4d1p4  42945  aks4d1p7  42949  isprimroot  42959  linvh  42962  primrootsunit1  42963  primrootscoprmpow  42965  primrootscoprbij  42968  sticksstones3  43014  aks6d1c6lem3  43038  grpods  43060  unitscyglem2  43062  unitscyglem4  43064  unitscyglem5  43065  supinf  43109  fsuppssindlem2  43438  infdesc  43489  isnacs  43549  elmzpcl  43571  mzpindd  43591  rencldnfilem  43661  irrapxlem6  43668  pellexlem3  43672  pellexlem5  43674  elpell1qr  43688  elpell14qr  43690  elpell1234qr  43692  pellfundre  43722  pellfundge  43723  pellfundlb  43725  pellfundglb  43726  rmspecnonsq  43748  jm2.22  43836  jm2.23  43837  rpnnen3lem  43872  fnwe2lem2  43892  elmnc  43977  dgraalem  43986  dgraaub  43989  mpaalem  43993  onsucelab  44104  limnsuc  44106  sqrtcvallem1  44471  rfovcnvf1od  44844  nzss  45141  iccshift  46348  iooshift  46352  limcperiod  46458  sumnnodd  46460  ioodvbdlimc1lem1  46759  dvnprodlem1  46774  dvnprodlem3  46776  itgperiod  46809  stoweidlem14  46842  stoweidlem15  46843  stoweidlem16  46844  stoweidlem31  46859  stoweidlem36  46864  stoweidlem46  46874  stoweidlem48  46876  fourierdlem2  46937  fourierdlem3  46938  fourierdlem20  46955  fourierdlem25  46960  fourierdlem37  46972  fourierdlem42  46977  fourierdlem48  46982  fourierdlem51  46985  fourierdlem63  46997  fourierdlem64  46998  fourierdlem65  46999  fourierdlem79  47013  fourierdlem81  47015  elaa2lem  47061  etransclem24  47086  etransclem26  47088  etransclem28  47090  etransclem35  47097  etransclem48  47110  salgenval  47149  salgenn0  47159  salgencl  47160  sssalgen  47163  salgenss  47164  salgenuni  47165  issalgend  47166  salgencntex  47171  subsaliuncllem  47185  sge0fodjrnlem  47244  meadjiunlem  47293  caragenel  47323  ovnlecvr  47386  ovnpnfelsup  47387  ovncvrrp  47392  ovnsubaddlem1  47398  hoidmv1lelem1  47419  hoidmv1lelem2  47420  hoidmv1lelem3  47421  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem4  47426  ovnhoilem1  47429  ovnlecvr2  47438  ovncvr2  47439  issmflem  47555  smflimlem2  47600  smflimlem3  47601  smflimsuplem2  47649  elsetpreimafvrab  48294  iccpart  48316  sprel  48384  prelspr  48386  sprsymrelfolem2  48393  sprsymrelf  48395  prpair  48401  paireqne  48411  prprelb  48416  prprelprb  48417  dfodd2  48552  dfeven5  48582  dfodd7  48583  fpprel  48644  clnbgrel  48744  clnbupgrel  48750  sclnbgrel  48763  vopnbgrel  48770  dfclnbgr6  48772  dfnbgr6  48773  isubgredg  48782  uhgrimisgrgric  48847  grtriprop  48857  isgrtri  48859  stgredgel  48873  stgrusgra  48875  uspgrlimlem3  48906  uspgrlim  48908  grlimgredgex  48916  grlimgrtrilem2  48918  gpgiedgdmel  48965  gpgedgel  48966  gpgnbgrvtx0  48990  gpgnbgrvtx1  48991  gpgprismgr4cycllem10  49020  1hegrlfgr  49048  assintop  49124  isassintop  49125  assintopcllaw  49127  0even  49152  2even  49154  2zrngamgm  49160  dmatALTbasel  49332  lcoval  49342  elbigo  49481  elrrx2linest2  49675  itsclc0  49701  itsclc0b  49702  itscnhlinecirc02p  49715  unilbss  49746  secval  50673  cscval  50674  cotval  50675  dvsec  50689  dvcsc  50690  dvcot  50691