Theorem elrab 3643

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {crab 3396  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439

This theorem is referenced by:  elrab3  3644  elrabd  3645  elrab2  3646  ralrab  3649  rexrab  3651  reurab  3656  rabsnt  4685  unimax  4897  ssintub  4918  intminss  4926  rabxfrd  5359  ssimaex  6916  weniso  7297  canth  7309  riotarab  7354  sorpsscmpl  7676  onnminsb  7741  dfom2  7807  ssnlim  7825  elsuppfng  8108  elsuppfn  8109  ressuppssdif  8124  oeeulem  8525  cofonr  8598  elpmg  8776  fineqvlem  9161  mapfienlem2  9301  supub  9354  suplub  9355  ordtypelem6  9420  ordtypelem7  9421  hartogslem1  9439  hartogs  9441  wemapsolem  9447  card2on  9451  elharval  9458  wdom2d  9477  cantnfs  9567  scottex  9789  tskwe  9854  cardid2  9857  iscard2  9880  cardmin2  9903  acni3  9949  alephsuc2  9982  kmlem1  10053  cofsmo  10171  coftr  10175  fin23lem11  10219  enfin2i  10223  fin1a2lem9  10310  fin1a2lem11  10312  axcc4  10341  axdc3lem2  10353  zorn2lem7  10404  ondomon  10465  alephval2  10474  grutsk  10724  negf1o  11558  infm3  12092  nnind  12154  peano2uz2  12571  peano5uzi  12572  dfuzi  12574  uzind  12575  uzind3  12577  eluz1  12746  uzind4  12810  nnwos  12819  eqreznegel  12838  zmin  12848  elixx1  13261  elioo2  13293  elfz1  13419  flval3  13726  serge0  13970  expge0  14012  expge1  14013  hashbclem  14366  pr2pwpr  14393  elss2prb  14402  hash2sspr  14403  wrdmap  14460  wwlktovfo  14872  shftf  14993  rlimrege0  15493  incexc2  15752  dvdsdivcl  16234  divalglem4  16314  divalgmod  16324  bitsval  16342  bezout  16461  dfgcd2  16464  lcmledvds  16517  lcmgcdlem  16524  lcmfledvds  16550  1nprm  16597  1idssfct  16598  isprm2  16600  hashdvds  16693  phisum  16709  odzval  16710  odzcllem  16711  odzdvds  16714  prmreclem2  16836  prmreclem5  16839  rami  16934  ramub1lem1  16945  ramub1lem2  16946  prmgaplem3  16972  prmgaplem4  16973  prmgaplem5  16974  prmgaplem6  16975  ismre  17500  ismri  17545  isacs  17565  isacs1i  17571  catlid  17597  catrid  17598  ismon  17648  isnat  17865  eldmcoa  17980  fncnvimaeqv  18034  lubeldm  18265  glbeldm  18278  gsumval2  18602  ismgmhm  18612  issubmgm  18618  rabsubmgmd  18620  mgmhmeql  18632  ismhm  18701  issubm  18719  issubmd  18722  mndind  18744  grplinv  18910  issubg  19047  isnsg  19075  cycsubg  19128  isgim  19182  isga  19211  elcntz  19242  elcntzsn  19245  symgfix2  19336  symgsssg  19387  symgfisg  19388  psgnunilem5  19414  odid  19458  odlem2  19459  gexid  19501  gexlem2  19502  gexdvds  19504  isslw  19528  pgpssslw  19534  pj1id  19619  oddvdssubg  19775  pgpfac1lem5  20001  ablfaclem2  20008  isirred  20346  isrnghm  20368  isrngim  20372  isrim0  20409  issubrng  20471  issubrg  20495  rgspnmin  20539  issdrg  20712  isabv  20735  islss  20876  islmhm  20970  islmim  21005  islbs  21019  psgndiflemB  21546  elocv  21614  isobs  21666  dsmmelbas  21685  frlmelbas  21702  islinds  21755  gsumbagdiaglem  21877  rhmpsrlem2  21888  psrlidm  21908  psrridm  21909  psrass1  21910  psrcom  21914  mplsubglem  21945  mpllsslem  21946  evlsval2  22033  ismhp  22074  ismhp3  22076  mhpmulcl  22083  psdmul  22100  coe1ae0  22148  coe1mul2  22202  dmatel  22428  scmatel  22440  scmateALT  22447  symgmatr01lem  22588  pmatcoe1fsupp  22636  cpmatel  22646  chpscmat  22777  istopon  22847  fctop  22939  cctop  22941  ppttop  22942  pptbas  22943  epttop  22944  iscld  22962  clscld  22982  isnei  23038  neips  23048  neiptopnei  23067  iscn  23170  iscnp  23172  cmpsublem  23334  conncompconn  23367  2ndc1stc  23386  2ndcdisj  23391  elkgen  23471  xkoccn  23554  txdis1cn  23570  txkgen  23587  xkococnlem  23594  xkococn  23595  xkoinjcn  23622  txconn  23624  elqtop  23632  elmptrab  23762  fbssfi  23772  opnfbas  23777  elfg  23806  cfinfil  23828  csdfil  23829  supfil  23830  filssufilg  23846  uffix  23856  fixufil  23857  uffixfr  23858  elflim2  23899  fclscf  23960  flimfnfcls  23963  alexsubALTlem2  23983  alexsubALTlem4  23985  alexsubALT  23986  ptcmplem2  23988  elutop  24168  isucn  24212  iscfilu  24222  ispsmet  24239  ismet  24258  isxmet  24259  elblps  24322  elbl  24323  restmetu  24505  icccmp  24761  elcncf  24829  ishtpy  24918  isphtpy  24927  om1elbas  24979  iscfil  25212  iscau  25223  iscmet  25231  lmle  25248  rrxfsupp  25349  minveclem3  25376  minveclem4  25379  ovolshftlem1  25457  ovolscalem1  25461  ovolicc2lem3  25467  dyadmax  25546  dyadmbllem  25547  opnmbllem  25549  vitalilem2  25557  vitalilem3  25558  elcpn  25883  ig1pval3  26130  coelem  26178  quotlem  26255  elqaalem1  26274  elqaalem3  26276  aannenlem1  26283  aannenlem2  26284  dmarea  26914  jensen  26946  ftalem4  27033  efnnfsumcl  27060  efchtdvds  27116  sqff1o  27139  fsumdvdsdiaglem  27140  dvdsppwf1o  27143  dvdsflf1o  27144  dvdsflsumcom  27145  musum  27148  muinv  27150  logfac2  27175  dchrelbas  27194  lgsfle1  27264  lgsle1  27270  lgsdirprm  27289  lgsne0  27293  lgsquadlem1  27338  lgsquadlem2  27339  dchrvmasumlem1  27453  logsqvma  27500  pntleml  27569  sltval2  27615  sltres  27621  conway  27760  scutcut  27762  scutbday  27765  scutun12  27771  scutbdaybnd2  27777  scutbdaylt  27779  bday1s  27795  cutlt  27896  precsexlem8  28172  precsexlem9  28173  precsexlem11  28175  onscutlt  28221  noseqinds  28243  peano5uzs  28348  uzsind  28349  tgellng  28551  mircgr  28655  mirbtwn  28656  iseqlg  28865  ttgelitv  28881  upgrle  29089  upgrbi  29092  umgredg2  29099  umgrbi  29100  edgupgr  29133  edgumgr  29134  upgredg  29136  numedglnl  29143  edgusgr  29159  usgruspgrb  29182  usgredg2ALT  29192  ushgredgedg  29228  ushgredgedgloop  29230  usgrexmplef  29258  upgrreslem  29303  umgrreslem  29304  upgrres1  29312  nbgrel  29339  nbupgrel  29344  nbumgrvtx  29345  nbusgreledg  29352  nbgrnself  29358  uvtxusgrel  29402  vtxdgoddnumeven  29553  rgrusgrprc  29589  lfgrwlkprop  29685  iswwlks  29835  iswwlksn  29837  wwlksnextsurj  29899  rusgrnumwwlkslem  29971  rusgrnumwwlks  29976  isclwwlk  29985  clwwlknscsh  30063  eleclclwwlkn  30077  clwlknf1oclwwlkn  30085  clwwlkvbij  30114  eupth2lems  30239  konigsberglem4  30256  fusgreg2wsplem  30334  2clwwlkel  30350  extwwlkfabel  30354  clwwlknonclwlknonf1o  30363  dlwwlknondlwlknonf1o  30366  numclwwlk2lem1  30377  numclwlk2lem2f  30378  numclwlk2lem2f1o  30380  grpoidinv2  30516  grpoinv  30526  isssp  30725  islno  30754  isblo  30783  ishmo  30812  ubthlem1  30871  ubthlem2  30872  htthlem  30918  ocel  31282  shsval2i  31388  ococin  31409  chsupsn  31414  eleigvec  31958  cnlnadjlem5  32072  shatomistici  32362  hatomistici  32363  dmrab  32497  elrabrd  32499  nnindf  32828  indf1ofs  32876  ismnt  32993  pwrssmgc  33010  tocycf  33127  tocyc01  33128  trsp2cyc  33133  cycpmco2f1  33134  cycpmco2rn  33135  cycpmco2lem2  33137  cycpmco2lem3  33138  cycpmco2lem5  33140  cycpmco2lem6  33141  cycpmco2lem7  33142  cycpmconjv  33152  tocyccntz  33154  cyc3evpm  33160  cycpmgcl  33163  cycpmconjslem2  33165  cyc3conja  33167  isfxp  33178  fxpgaeq  33179  elrgspnsubrun  33259  fldgensdrg  33324  nsgmgclem  33420  nsgmgc  33421  nsgqusf1olem2  33423  isprmidl  33447  ismxidl  33471  ssmxidl  33483  isrprm  33526  1arithufdlem3  33555  1arithufdlem4  33556  1arithufd  33557  mplvrpmlem  33636  mplvrpmga  33638  mplvrpmmhm  33639  fedgmullem2  33715  ply1annnr  33788  minplyann  33794  minplyirred  33796  constrsuc  33823  zarclsiin  33956  zart0  33964  rhmpreimacnlem  33969  ordtconnlem1  34009  sigagenval  34225  ldsysgenld  34245  ldgenpisyslem1  34248  ldgenpisyslem2  34249  ldgenpisys  34251  ddemeas  34321  ismbfm  34336  imambfm  34347  dya2iocuni  34368  oms0  34382  omssubadd  34385  elcarsg  34390  issibf  34418  sitgfval  34426  oddpwdc  34439  eulerpartlemgh  34463  eulerpartlemgs2  34465  dstfrvel  34559  ballotlemfc0  34578  ballotlemfcc  34579  ballotlemiex  34587  ballotlemfrcn0  34615  ballotlemirc  34617  ballotlem7  34621  reprsum  34698  reprsuc  34700  reprpmtf1o  34711  reprdifc  34712  fnrelpredd  35174  fineqvnttrclselem2  35214  connpconn  35351  iscvm  35375  cvmsi  35381  cvmsval  35382  cvmliftmolem2  35398  cvmliftiota  35417  snmlval  35447  satfv1lem  35478  fmlafvel  35501  fmla1  35503  fmlaomn0  35506  satfv0fvfmla0  35529  sategoelfvb  35535  elmpst  35652  lineelsb2  36264  linerflx1  36265  fwddifval  36278  fwddifnval  36279  rankeq1o  36287  finminlem  36434  fneint  36464  fnessref  36473  topmeet  36480  topjoin  36481  neifg  36487  weiunlem2  36579  weiunfrlem  36580  weiunse  36584  relowlssretop  37480  fin2solem  37719  fin2so  37720  poimirlem4  37737  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  poimirlem31  37764  poimirlem32  37765  opnmbllem0  37769  mblfinlem2  37771  itg2gt0cn  37788  indexa  37846  nninfnub  37864  istotbnd  37882  sstotbnd2  37887  isbnd  37893  isrngohom  38078  isrngoiso  38091  isidl  38127  ispridl  38147  ismaxidl  38153  prnc  38180  isfldidl  38181  islshp  39151  lssats  39184  islfl  39232  isat  39458  atlatmstc  39491  islln  39678  islpln  39702  islvol  39745  linepsubN  39924  elpmap  39930  pmapsub  39940  elpadd  39971  paddvaln0N  39973  islhp  40168  isldil  40282  isltrn  40291  isdilN  40326  istrnN  40329  diaval  41204  diaelval  41205  diaeldm  41208  diaelrnN  41217  cdlemm10N  41290  docaclN  41296  dibglbN  41338  dicval  41348  dicfnN  41355  dicvalrelN  41357  dihglblem2aN  41465  dihglblem2N  41466  dihglblem3N  41467  dih1dimatlem  41501  dihglb2  41514  dochvalr  41529  doch2val2  41536  dochocss  41538  islpolN  41655  mapd0  41837  aks4d1p4  42245  aks4d1p7  42249  isprimroot  42259  linvh  42262  primrootsunit1  42263  primrootscoprmpow  42265  primrootscoprbij  42268  sticksstones3  42314  aks6d1c6lem3  42338  grpods  42360  unitscyglem2  42362  unitscyglem4  42364  unitscyglem5  42365  supinf  42412  fsuppssindlem2  42750  infdesc  42801  isnacs  42861  elmzpcl  42883  mzpindd  42903  rencldnfilem  42977  irrapxlem6  42984  pellexlem3  42988  pellexlem5  42990  elpell1qr  43004  elpell14qr  43006  elpell1234qr  43008  pellfundre  43038  pellfundge  43039  pellfundlb  43041  pellfundglb  43042  rmspecnonsq  43064  jm2.22  43152  jm2.23  43153  rpnnen3lem  43188  fnwe2lem2  43208  elmnc  43293  dgraalem  43302  dgraaub  43305  mpaalem  43309  onsucelab  43420  limnsuc  43422  sqrtcvallem1  43788  rfovcnvf1od  44161  scottelrankd  44404  nzss  44474  iccshift  45680  iooshift  45684  limcperiod  45790  sumnnodd  45792  ioodvbdlimc1lem1  46091  dvnprodlem1  46106  dvnprodlem3  46108  itgperiod  46141  stoweidlem14  46174  stoweidlem15  46175  stoweidlem16  46176  stoweidlem31  46191  stoweidlem36  46196  stoweidlem46  46206  stoweidlem48  46208  fourierdlem2  46269  fourierdlem3  46270  fourierdlem20  46287  fourierdlem25  46292  fourierdlem37  46304  fourierdlem42  46309  fourierdlem48  46314  fourierdlem51  46317  fourierdlem63  46329  fourierdlem64  46330  fourierdlem65  46331  fourierdlem79  46345  fourierdlem81  46347  elaa2lem  46393  etransclem24  46418  etransclem26  46420  etransclem28  46422  etransclem35  46429  etransclem48  46442  salgenval  46481  salgenn0  46491  salgencl  46492  sssalgen  46495  salgenss  46496  salgenuni  46497  issalgend  46498  salgencntex  46503  subsaliuncllem  46517  sge0fodjrnlem  46576  meadjiunlem  46625  caragenel  46655  ovnlecvr  46718  ovnpnfelsup  46719  ovncvrrp  46724  ovnsubaddlem1  46730  hoidmv1lelem1  46751  hoidmv1lelem2  46752  hoidmv1lelem3  46753  hoidmvlelem1  46755  hoidmvlelem2  46756  hoidmvlelem4  46758  ovnhoilem1  46761  ovnlecvr2  46770  ovncvr2  46771  issmflem  46887  smflimlem2  46932  smflimlem3  46933  smflimsuplem2  46981  elsetpreimafvrab  47556  iccpart  47578  sprel  47646  prelspr  47648  sprsymrelfolem2  47655  sprsymrelf  47657  prpair  47663  paireqne  47673  prprelb  47678  prprelprb  47679  dfodd2  47798  dfeven5  47828  dfodd7  47829  fpprel  47890  clnbgrel  47990  clnbupgrel  47996  sclnbgrel  48009  vopnbgrel  48016  dfclnbgr6  48018  dfnbgr6  48019  isubgredg  48028  uhgrimisgrgric  48093  grtriprop  48103  isgrtri  48105  stgredgel  48119  stgrusgra  48121  uspgrlimlem3  48152  uspgrlim  48154  grlimgredgex  48162  grlimgrtrilem2  48164  gpgiedgdmel  48211  gpgedgel  48212  gpgnbgrvtx0  48236  gpgnbgrvtx1  48237  gpgprismgr4cycllem10  48266  1hegrlfgr  48294  assintop  48371  isassintop  48372  assintopcllaw  48374  0even  48399  2even  48401  2zrngamgm  48407  dmatALTbasel  48564  lcoval  48574  elbigo  48713  elrrx2linest2  48907  itsclc0  48933  itsclc0b  48934  itscnhlinecirc02p  48947  unilbss  48979  secval  49908  cscval  49909  cotval  49910