Theorem elrab 3585

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   = wceq 1656   ∈ wcel 2164  {crab 3121  Vcvv 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416

This theorem is referenced by:  elrab3  3587  elrabd  3588  elrab2  3589  ralrab  3591  rexrab  3593  rabsnt  4486  unimax  4697  ssintub  4717  intminss  4725  rabxfrd  5119  ssimaex  6514  weniso  6864  canth  6868  sorpsscmpl  7213  onnminsb  7270  dfom2  7333  ssnlim  7349  elsuppfn  7572  ressuppssdif  7585  oeeulem  7953  nnawordex  7989  elpmg  8143  fineqvlem  8449  mapfienlem2  8586  supub  8640  suplub  8641  ordtypelem6  8704  ordtypelem7  8705  hartogslem1  8723  hartogs  8725  wemapsolem  8731  card2on  8735  elharval  8744  wdom2d  8761  cantnfs  8847  oemapvali  8865  rankuni2b  9000  scottex  9032  tskwe  9096  cardid2  9099  iscard2  9122  harval2  9143  cardmin2  9144  acni3  9190  alephsuc2  9223  kmlem1  9294  cofsmo  9413  coftr  9417  fin23lem11  9461  enfin2i  9465  fin1a2lem9  9552  fin1a2lem11  9554  axcc4  9583  axdc3lem2  9595  zorn2lem7  9646  ondomon  9707  alephval2  9716  grutsk  9966  pinq  10071  negf1o  10791  fiminre  11309  infm3  11319  nnind  11377  peano2uz2  11800  peano5uzi  11801  dfuzi  11803  uzind  11804  uzind3  11806  eluz1  11979  uzind4  12035  nnwos  12045  eqreznegel  12064  zsupss  12067  zmin  12074  elixx1  12479  elioo2  12511  elfz1  12631  flval3  12918  serge0  13156  expge0  13197  expge1  13198  hashbclem  13532  pr2pwpr  13557  elss2prb  13565  hash2sspr  13566  wrdmap  13613  wwlktovfo  14087  shftf  14203  rlimrege0  14694  incexc2  14951  dvdsdivcl  15422  divalglem4  15500  divalgmod  15510  bitsval  15526  bezout  15640  dfgcd2  15643  lcmledvds  15692  lcmgcdlem  15699  lcmfledvds  15725  1nprm  15771  1idssfct  15772  isprm2  15774  phicl2  15851  hashdvds  15858  phisum  15873  odzval  15874  odzcllem  15875  odzdvds  15878  pcpremul  15926  prmreclem1  15998  prmreclem2  15999  prmreclem3  16000  prmreclem5  16002  ramub  16095  rami  16097  ramub1lem1  16108  ramub1lem2  16109  prmgaplem3  16135  prmgaplem4  16136  prmgaplem5  16137  prmgaplem6  16138  ismre  16610  mrcflem  16626  mrcval  16630  ismri  16651  isacs  16671  isacs1i  16677  catlid  16703  catrid  16704  ismon  16752  isnat  16966  eldmcoa  17074  coaval  17077  fncnvimaeqv  17119  lubeldm  17341  glbeldm  17354  gsumval2  17640  ismhm  17697  issubm  17707  issubmd  17709  mhmeql  17724  mrcmndind  17726  grplinv  17829  issubg  17952  cycsubg  17980  isnsg  17981  ghmeql  18041  isgim  18062  isga  18081  elcntz  18112  elcntzsn  18115  symgfix2  18193  pmtrval  18228  pmtrrn  18234  symgsssg  18244  symgfisg  18245  psgnunilem5  18271  psgnunilem5OLD  18272  odid  18315  odlem2  18316  gexid  18354  gexlem2  18355  gexdvds  18357  isslw  18381  pgpssslw  18387  pj1id  18470  efgsfo  18511  oddvdssubg  18618  dprdwd  18771  pgpfac1lem5  18839  ablfaclem2  18846  isirred  19060  isrim0  19086  issubrg  19143  isabv  19182  islss  19298  islmhm  19393  lmhmeql  19421  islmim  19428  islbs  19442  gsumbagdiaglem  19743  psrmulcllem  19755  psrlidm  19771  psrridm  19772  psrass1  19773  psrcom  19777  mplsubglem  19802  mpllsslem  19803  mplmonmul  19832  evlsval2  19887  coe1fsupp  19951  coe1ae0  19953  coe1mul2  20006  zrhcofipsgnOLD  20306  psgndiflemB  20313  elocv  20382  isobs  20434  dsmmelbas  20453  frlmelbas  20470  frlmssuvc2  20508  islinds  20522  dmatel  20674  dmatmulcl  20681  scmatel  20686  scmateALT  20693  symgmatr01lem  20835  pmatcoe1fsupp  20883  cpmatel  20893  chpscmat  21024  istopon  21094  fctop  21186  cctop  21188  ppttop  21189  pptbas  21190  epttop  21191  iscld  21209  clscld  21229  isnei  21285  neips  21295  neiptopnei  21314  iscn  21417  iscnp  21419  ordthauslem  21565  cmpsublem  21580  conncompconn  21613  2ndc1stc  21632  2ndcdisj  21637  locfincmp  21707  elkgen  21717  xkoopn  21770  xkoccn  21800  txdis1cn  21816  pthaus  21819  txkgen  21833  xkohaus  21834  xkococnlem  21840  xkococn  21841  xkoinjcn  21868  txconn  21870  elqtop  21878  nrmr0reg  21930  elmptrab  22008  fbssfi  22018  opnfbas  22023  elfg  22052  cfinfil  22074  csdfil  22075  supfil  22076  filssufilg  22092  uffix  22102  fixufil  22103  uffixfr  22104  uffixsn  22106  ufinffr  22110  ufilen  22111  elflim2  22145  supnfcls  22201  fclscf  22206  flimfnfcls  22209  alexsubALTlem2  22229  alexsubALTlem4  22231  alexsubALT  22232  ptcmplem2  22234  tmdgsum2  22277  symgtgp  22282  ghmcnp  22295  elutop  22414  isucn  22459  iscfilu  22469  ispsmet  22486  ismet  22505  isxmet  22506  elblps  22569  elbl  22570  restmetu  22752  icccmp  23005  elcncf  23069  ishtpy  23148  isphtpy  23157  om1elbas  23208  iscfil  23440  iscau  23451  iscmet  23459  lmle  23476  rrxfsupp  23577  minveclem3  23604  minveclem4  23607  ovolshftlem1  23682  ovolscalem1  23686  ovolicc2lem3  23692  iundisj  23721  dyadmax  23771  dyadmbllem  23772  opnmbllem  23774  vitalilem2  23782  vitalilem3  23783  elcpn  24103  ig1pval3  24340  coelem  24388  quotlem  24461  elqaalem1  24480  elqaalem3  24482  aannenlem1  24489  aannenlem2  24490  aalioulem2  24494  radcnv0  24576  dmarea  25104  jensen  25135  ftalem4  25222  ftalem5  25223  efnnfsumcl  25249  efchtdvds  25305  sqff1o  25328  fsumdvdsdiaglem  25329  dvdsppwf1o  25332  dvdsflf1o  25333  dvdsflsumcom  25334  musum  25337  muinv  25339  logfac2  25362  dchrelbas  25381  dchrfi  25400  lgsfle1  25451  lgsle1  25457  lgsdirprm  25476  lgsne0  25480  lgsquadlem1  25525  lgsquadlem2  25526  2lgslem1b  25537  dchrvmasumlem1  25604  logsqvma  25651  pntleml  25720  tgellng  25872  mircgr  25976  mirbtwn  25977  iseqlg  26173  ttgelitv  26189  upgrle  26395  upgrbi  26398  umgredg2  26405  umgrbi  26406  upgr1elem  26417  edgupgr  26439  edgumgr  26440  upgredg  26443  numedglnl  26450  edgusgr  26466  usgruspgrb  26487  usgredg2ALT  26496  ushgredgedg  26532  ushgredgedgloop  26534  ushgredgedgloopOLD  26535  usgrexmplef  26563  subumgredg2  26589  subupgr  26591  upgrreslem  26608  umgrreslem  26609  upgrres1  26617  nbgrel  26644  nbupgrel  26649  nbumgrvtx  26650  nbusgreledg  26657  nbgrnself  26663  uvtxusgrel  26708  1hevtxdg1  26811  umgr2v2e  26830  vtxdgoddnumeven  26858  rgrusgrprc  26894  rgrx0ndm  26898  lfgrwlkprop  26995  iswwlks  27142  iswwlksn  27144  wwlksn0  27169  wlknwwlksnsurOLD  27197  wlkwwlksurOLD  27205  wwlksnextsurj  27221  wwlksnextsurOLD  27226  wlksnwwlknvbijOLD  27238  rusgrnumwwlkslem  27305  rusgrnumwwlks  27310  rusgrnumwwlksOLD  27311  isclwwlk  27320  clwwlknscsh  27415  eleclclwwlkn  27429  clwlknf1oclwwlkn  27451  clwlknf1oclwwlknOLD  27453  s2elclwwlknon2  27475  clwwlkvbij  27484  clwwlkvbijOLD  27485  eupth2lems  27611  konigsberglem4  27630  fusgreg2wsplem  27710  2clwwlkel  27729  numclwwlkovgelOLD  27733  extwwlkfabel  27738  extwwlkfabelOLD  27739  clwwlknonclwlknonf1o  27756  clwwlknonclwlknonf1oOLD  27757  dlwwlknondlwlknonf1o  27762  dlwwlknondlwlknonf1oOLD  27763  numclwwlk2lem1  27775  numclwlk2lem2f  27776  numclwlk2lem2f1o  27778  numclwlk2lem2fOLD  27779  numclwlk2lem2f1oOLD  27781  numclwwlk2lem1OLD  27786  numclwlk2lem2fOLDOLD  27787  numclwlk2lem2f1oOLDOLD  27789  grpoidinv2  27921  grpoinv  27931  isssp  28130  islno  28159  isblo  28188  ishmo  28217  ubthlem1  28277  ubthlem2  28278  htthlem  28325  ocel  28691  shsval2i  28797  ococin  28818  chsupsn  28823  eleigvec  29367  cnlnadjlem5  29481  shatomistici  29771  hatomistici  29772  nnindf  30108  ordtconnlem1  30511  indf1ofs  30629  sigagenval  30744  ldsysgenld  30764  ldgenpisyslem1  30767  ldgenpisyslem2  30768  ldgenpisys  30770  ddemeas  30840  ismbfm  30855  imambfm  30865  dya2iocuni  30886  oms0  30900  omssubadd  30903  elcarsg  30908  issibf  30936  sitgfval  30944  oddpwdc  30957  eulerpartlemgh  30981  eulerpartlemgs2  30983  dstfrvel  31077  ballotlemfc0  31096  ballotlemfcc  31097  ballotlemiex  31105  ballotlemfrcn0  31133  ballotlemirc  31135  ballotlem7  31139  reprsum  31236  reprsuc  31238  reprpmtf1o  31249  reprdifc  31250  connpconn  31759  iscvm  31783  cvmsi  31789  cvmsval  31790  cvmliftmolem2  31806  cvmliftiota  31825  snmlval  31855  elmpst  31975  sltval2  32343  sltres  32349  conway  32444  scutcut  32446  scutbday  32447  scutun12  32451  scutbdaybnd  32455  scutbdaylt  32456  lineelsb2  32789  linerflx1  32790  fwddifval  32803  fwddifnval  32804  rankeq1o  32812  finminlem  32846  fneint  32876  fnessref  32885  topmeet  32892  topjoin  32893  neifg  32899  relowlssretop  33755  fin2solem  33937  fin2so  33938  poimirlem4  33956  poimirlem25  33977  poimirlem26  33978  poimirlem27  33979  poimirlem31  33983  poimirlem32  33984  opnmbllem0  33988  mblfinlem2  33990  itg2gt0cn  34007  indexa  34070  nninfnub  34088  istotbnd  34109  sstotbnd2  34114  isbnd  34120  isrngohom  34305  isrngoiso  34318  isidl  34354  ispridl  34374  ismaxidl  34380  prnc  34407  isfldidl  34408  islshp  35053  lssats  35086  islfl  35134  isat  35360  atlatmstc  35393  islln  35580  islpln  35604  islvol  35647  linepsubN  35826  elpmap  35832  pmapsub  35842  elpadd  35873  paddvaln0N  35875  islhp  36070  isldil  36184  isltrn  36193  isdilN  36228  istrnN  36231  diaval  37106  diaelval  37107  diaeldm  37110  diaelrnN  37119  cdlemm10N  37192  docaclN  37198  dibglbN  37240  dicval  37250  dicfnN  37257  dicvalrelN  37259  dihglblem2aN  37367  dihglblem2N  37368  dihglblem3N  37369  dih1dimatlem  37403  dihglb2  37416  dochvalr  37431  doch2val2  37438  dochocss  37440  islpolN  37557  mapd0  37739  isnacs  38110  elmzpcl  38132  mzpindd  38152  rencldnfilem  38227  irrapxlem6  38234  pellexlem3  38238  pellexlem5  38240  elpell1qr  38254  elpell14qr  38256  elpell1234qr  38258  pellfundre  38288  pellfundge  38289  pellfundlb  38291  pellfundglb  38292  rmspecnonsq  38314  jm2.22  38404  jm2.23  38405  rpnnen3lem  38440  fnwe2lem2  38463  fnwe2lem3  38464  elmnc  38548  dgraalem  38557  dgraaub  38560  mpaalem  38564  rgspnmin  38583  issdrg  38609  rfovcnvf1od  39137  nzss  39355  iccshift  40538  iooshift  40542  limcperiod  40653  sumnnodd  40655  ioodvbdlimc1lem1  40939  dvnprodlem1  40954  dvnprodlem3  40956  itgperiod  40989  stoweidlem14  41023  stoweidlem15  41024  stoweidlem16  41025  stoweidlem31  41040  stoweidlem36  41045  stoweidlem46  41055  stoweidlem48  41057  fourierdlem2  41118  fourierdlem3  41119  fourierdlem20  41136  fourierdlem25  41141  fourierdlem37  41153  fourierdlem42  41158  fourierdlem48  41163  fourierdlem51  41166  fourierdlem63  41178  fourierdlem64  41179  fourierdlem65  41180  fourierdlem79  41194  fourierdlem81  41196  elaa2lem  41242  etransclem24  41267  etransclem26  41269  etransclem28  41271  etransclem35  41278  etransclem48  41291  salgenval  41330  salgenn0  41338  salgencl  41339  sssalgen  41342  salgenss  41343  salgenuni  41344  issalgend  41345  salgencntex  41350  subsaliuncllem  41364  sge0fodjrnlem  41422  meadjiunlem  41471  caragenel  41501  ovnlecvr  41564  ovnpnfelsup  41565  ovncvrrp  41570  ovnsubaddlem1  41576  hoidmv1lelem1  41597  hoidmv1lelem2  41598  hoidmv1lelem3  41599  hoidmvlelem1  41601  hoidmvlelem2  41602  hoidmvlelem4  41604  ovnhoilem1  41607  ovnlecvr2  41616  ovncvr2  41617  issmflem  41728  smflimlem2  41772  smflimlem3  41773  smflimsuplem2  41819  iccpart  42238  prpair  42267  pairreueq  42278  paireqne  42279  dfodd2  42397  dfeven5  42426  dfodd7  42427  1hegrlfgr  42578  sprel  42599  prelspr  42601  sprsymrelfolem2  42608  sprsymrelf  42610  ismgmhm  42648  issubmgm  42654  rabsubmgmd  42656  mgmhmeql  42668  assintop  42710  isassintop  42711  assintopcllaw  42713  isrnghm  42757  isrngisom  42761  0even  42796  2even  42798  2zrngamgm  42804  dmatALTbasel  43056  lcoval  43066  elbigo  43210  itsclc0  43327  secval  43400  cscval  43401  cotval  43402