Theorem elrab 3617

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {crab 3067  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424

This theorem is referenced by:  elrab3  3618  elrabd  3619  elrab2  3620  ralrab  3623  rexrab  3626  rabsnt  4664  unimax  4874  ssintub  4894  intminss  4902  rabxfrd  5335  ssimaex  6835  weniso  7205  canth  7209  sorpsscmpl  7565  onnminsb  7626  dfom2  7689  ssnlim  7707  elsuppfng  7957  elsuppfn  7958  ressuppssdif  7972  oeeulem  8394  elpmg  8589  fineqvlem  8966  mapfienlem2  9095  supub  9148  suplub  9149  ordtypelem6  9212  ordtypelem7  9213  hartogslem1  9231  hartogs  9233  wemapsolem  9239  card2on  9243  elharval  9250  wdom2d  9269  cantnfs  9354  scottex  9574  tskwe  9639  cardid2  9642  iscard2  9665  cardmin2  9688  acni3  9734  alephsuc2  9767  kmlem1  9837  cofsmo  9956  coftr  9960  fin23lem11  10004  enfin2i  10008  fin1a2lem9  10095  fin1a2lem11  10097  axcc4  10126  axdc3lem2  10138  zorn2lem7  10189  ondomon  10250  alephval2  10259  grutsk  10509  negf1o  11335  infm3  11864  nnind  11921  peano2uz2  12338  peano5uzi  12339  dfuzi  12341  uzind  12342  uzind3  12344  eluz1  12515  uzind4  12575  nnwos  12584  eqreznegel  12603  zmin  12613  elixx1  13017  elioo2  13049  elfz1  13173  flval3  13463  serge0  13705  expge0  13747  expge1  13748  hashbclem  14092  pr2pwpr  14121  elss2prb  14129  hash2sspr  14130  wrdmap  14177  wwlktovfo  14601  shftf  14718  rlimrege0  15216  incexc2  15478  dvdsdivcl  15953  divalglem4  16033  divalgmod  16043  bitsval  16059  bezout  16179  dfgcd2  16182  lcmledvds  16232  lcmgcdlem  16239  lcmfledvds  16265  1nprm  16312  1idssfct  16313  isprm2  16315  hashdvds  16404  phisum  16419  odzval  16420  odzcllem  16421  odzdvds  16424  prmreclem2  16546  prmreclem5  16549  rami  16644  ramub1lem1  16655  ramub1lem2  16656  prmgaplem3  16682  prmgaplem4  16683  prmgaplem5  16684  prmgaplem6  16685  ismre  17216  ismri  17257  isacs  17277  isacs1i  17283  catlid  17309  catrid  17310  ismon  17362  isnat  17579  eldmcoa  17696  fncnvimaeqv  17752  lubeldm  17986  glbeldm  17999  gsumval2  18285  ismhm  18347  issubm  18357  issubmd  18360  mndind  18381  grplinv  18543  issubg  18670  isnsg  18698  cycsubg  18742  isgim  18793  isga  18812  elcntz  18843  elcntzsn  18846  symgfix2  18939  symgsssg  18990  symgfisg  18991  psgnunilem5  19017  odid  19061  odlem2  19062  gexid  19101  gexlem2  19102  gexdvds  19104  isslw  19128  pgpssslw  19134  pj1id  19220  oddvdssubg  19371  pgpfac1lem5  19597  ablfaclem2  19604  isirred  19856  isrim0  19882  issubrg  19939  issdrg  19978  isabv  19994  islss  20111  islmhm  20204  islmim  20239  islbs  20253  psgndiflemB  20717  elocv  20785  isobs  20837  dsmmelbas  20856  frlmelbas  20873  islinds  20926  gsumbagdiaglemOLD  21051  gsumbagdiaglem  21054  psrmulcllem  21066  psrlidm  21082  psrridm  21083  psrass1  21084  psrcom  21088  mplsubglem  21115  mpllsslem  21116  evlsval2  21207  ismhp  21241  ismhp3  21243  mhpmulcl  21249  coe1ae0  21297  coe1mul2  21350  dmatel  21550  scmatel  21562  scmateALT  21569  symgmatr01lem  21710  pmatcoe1fsupp  21758  cpmatel  21768  chpscmat  21899  istopon  21969  fctop  22062  cctop  22064  ppttop  22065  pptbas  22066  epttop  22067  iscld  22086  clscld  22106  isnei  22162  neips  22172  neiptopnei  22191  iscn  22294  iscnp  22296  cmpsublem  22458  conncompconn  22491  2ndc1stc  22510  2ndcdisj  22515  elkgen  22595  xkoccn  22678  txdis1cn  22694  txkgen  22711  xkococnlem  22718  xkococn  22719  xkoinjcn  22746  txconn  22748  elqtop  22756  elmptrab  22886  fbssfi  22896  opnfbas  22901  elfg  22930  cfinfil  22952  csdfil  22953  supfil  22954  filssufilg  22970  uffix  22980  fixufil  22981  uffixfr  22982  elflim2  23023  fclscf  23084  flimfnfcls  23087  alexsubALTlem2  23107  alexsubALTlem4  23109  alexsubALT  23110  ptcmplem2  23112  elutop  23293  isucn  23338  iscfilu  23348  ispsmet  23365  ismet  23384  isxmet  23385  elblps  23448  elbl  23449  restmetu  23632  icccmp  23894  elcncf  23958  ishtpy  24041  isphtpy  24050  om1elbas  24101  iscfil  24334  iscau  24345  iscmet  24353  lmle  24370  rrxfsupp  24471  minveclem3  24498  minveclem4  24501  ovolshftlem1  24578  ovolscalem1  24582  ovolicc2lem3  24588  dyadmax  24667  dyadmbllem  24668  opnmbllem  24670  vitalilem2  24678  vitalilem3  24679  elcpn  25003  ig1pval3  25244  coelem  25292  quotlem  25365  elqaalem1  25384  elqaalem3  25386  aannenlem1  25393  aannenlem2  25394  dmarea  26012  jensen  26043  ftalem4  26130  efnnfsumcl  26157  efchtdvds  26213  sqff1o  26236  fsumdvdsdiaglem  26237  dvdsppwf1o  26240  dvdsflf1o  26241  dvdsflsumcom  26242  musum  26245  muinv  26247  logfac2  26270  dchrelbas  26289  lgsfle1  26359  lgsle1  26365  lgsdirprm  26384  lgsne0  26388  lgsquadlem1  26433  lgsquadlem2  26434  dchrvmasumlem1  26548  logsqvma  26595  pntleml  26664  tgellng  26818  mircgr  26922  mirbtwn  26923  iseqlg  27132  ttgelitv  27153  upgrle  27363  upgrbi  27366  umgredg2  27373  umgrbi  27374  edgupgr  27407  edgumgr  27408  upgredg  27410  numedglnl  27417  edgusgr  27433  usgruspgrb  27454  usgredg2ALT  27463  ushgredgedg  27499  ushgredgedgloop  27501  usgrexmplef  27529  upgrreslem  27574  umgrreslem  27575  upgrres1  27583  nbgrel  27610  nbupgrel  27615  nbumgrvtx  27616  nbusgreledg  27623  nbgrnself  27629  uvtxusgrel  27673  vtxdgoddnumeven  27823  rgrusgrprc  27859  lfgrwlkprop  27957  iswwlks  28102  iswwlksn  28104  wwlksnextsurj  28166  rusgrnumwwlkslem  28235  rusgrnumwwlks  28240  isclwwlk  28249  clwwlknscsh  28327  eleclclwwlkn  28341  clwlknf1oclwwlkn  28349  clwwlkvbij  28378  eupth2lems  28503  konigsberglem4  28520  fusgreg2wsplem  28598  2clwwlkel  28614  extwwlkfabel  28618  clwwlknonclwlknonf1o  28627  dlwwlknondlwlknonf1o  28630  numclwwlk2lem1  28641  numclwlk2lem2f  28642  numclwlk2lem2f1o  28644  grpoidinv2  28778  grpoinv  28788  isssp  28987  islno  29016  isblo  29045  ishmo  29074  ubthlem1  29133  ubthlem2  29134  htthlem  29180  ocel  29544  shsval2i  29650  ococin  29671  chsupsn  29676  eleigvec  30220  cnlnadjlem5  30334  shatomistici  30624  hatomistici  30625  dmrab  30745  nnindf  31035  ismnt  31163  pwrssmgc  31180  tocycf  31286  tocyc01  31287  trsp2cyc  31292  cycpmco2f1  31293  cycpmco2rn  31294  cycpmco2lem2  31296  cycpmco2lem3  31297  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmconjv  31311  tocyccntz  31313  cyc3evpm  31319  cycpmgcl  31322  cycpmconjslem2  31324  cyc3conja  31326  nsgmgclem  31498  nsgmgc  31499  nsgqusf1olem2  31501  isprmidl  31515  ismxidl  31536  ssmxidl  31544  isrprm  31567  fedgmullem2  31613  zarclsiin  31723  zart0  31731  rhmpreimacnlem  31736  ordtconnlem1  31776  indf1ofs  31894  sigagenval  32008  ldsysgenld  32028  ldgenpisyslem1  32031  ldgenpisyslem2  32032  ldgenpisys  32034  ddemeas  32104  ismbfm  32119  imambfm  32129  dya2iocuni  32150  oms0  32164  omssubadd  32167  elcarsg  32172  issibf  32200  sitgfval  32208  oddpwdc  32221  eulerpartlemgh  32245  eulerpartlemgs2  32247  dstfrvel  32340  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemiex  32368  ballotlemfrcn0  32396  ballotlemirc  32398  ballotlem7  32402  reprsum  32493  reprsuc  32495  reprpmtf1o  32506  reprdifc  32507  fnrelpredd  32961  connpconn  33097  iscvm  33121  cvmsi  33127  cvmsval  33128  cvmliftmolem2  33144  cvmliftiota  33163  snmlval  33193  satfv1lem  33224  fmlafvel  33247  fmla1  33249  fmlaomn0  33252  satfv0fvfmla0  33275  sategoelfvb  33281  elmpst  33398  riotarab  33575  reurab  33576  sltval2  33786  sltres  33792  conway  33920  scutcut  33922  scutbday  33925  scutun12  33931  scutbdaybnd2  33937  scutbdaylt  33939  bday1s  33952  lineelsb2  34377  linerflx1  34378  fwddifval  34391  fwddifnval  34392  rankeq1o  34400  finminlem  34434  fneint  34464  fnessref  34473  topmeet  34480  topjoin  34481  neifg  34487  relowlssretop  35461  fin2solem  35690  fin2so  35691  poimirlem4  35708  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem31  35735  poimirlem32  35736  opnmbllem0  35740  mblfinlem2  35742  itg2gt0cn  35759  indexa  35818  nninfnub  35836  istotbnd  35854  sstotbnd2  35859  isbnd  35865  isrngohom  36050  isrngoiso  36063  isidl  36099  ispridl  36119  ismaxidl  36125  prnc  36152  isfldidl  36153  islshp  36920  lssats  36953  islfl  37001  isat  37227  atlatmstc  37260  islln  37447  islpln  37471  islvol  37514  linepsubN  37693  elpmap  37699  pmapsub  37709  elpadd  37740  paddvaln0N  37742  islhp  37937  isldil  38051  isltrn  38060  isdilN  38095  istrnN  38098  diaval  38973  diaelval  38974  diaeldm  38977  diaelrnN  38986  cdlemm10N  39059  docaclN  39065  dibglbN  39107  dicval  39117  dicfnN  39124  dicvalrelN  39126  dihglblem2aN  39234  dihglblem2N  39235  dihglblem3N  39236  dih1dimatlem  39270  dihglb2  39283  dochvalr  39298  doch2val2  39305  dochocss  39307  islpolN  39424  mapd0  39606  aks4d1p4  40015  aks4d1p7  40019  sticksstones3  40032  fsuppssindlem2  40204  infdesc  40396  isnacs  40442  elmzpcl  40464  mzpindd  40484  rencldnfilem  40558  irrapxlem6  40565  pellexlem3  40569  pellexlem5  40571  elpell1qr  40585  elpell14qr  40587  elpell1234qr  40589  pellfundre  40619  pellfundge  40620  pellfundlb  40622  pellfundglb  40623  rmspecnonsq  40645  jm2.22  40733  jm2.23  40734  rpnnen3lem  40769  fnwe2lem2  40792  elmnc  40877  dgraalem  40886  dgraaub  40889  mpaalem  40893  rgspnmin  40912  sqrtcvallem1  41128  rfovcnvf1od  41501  scottelrankd  41754  nzss  41824  iccshift  42946  iooshift  42950  limcperiod  43059  sumnnodd  43061  ioodvbdlimc1lem1  43362  dvnprodlem1  43377  dvnprodlem3  43379  itgperiod  43412  stoweidlem14  43445  stoweidlem15  43446  stoweidlem16  43447  stoweidlem31  43462  stoweidlem36  43467  stoweidlem46  43477  stoweidlem48  43479  fourierdlem2  43540  fourierdlem3  43541  fourierdlem20  43558  fourierdlem25  43563  fourierdlem37  43575  fourierdlem42  43580  fourierdlem48  43585  fourierdlem51  43588  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem79  43616  fourierdlem81  43618  elaa2lem  43664  etransclem24  43689  etransclem26  43691  etransclem28  43693  etransclem35  43700  etransclem48  43713  salgenval  43752  salgenn0  43760  salgencl  43761  sssalgen  43764  salgenss  43765  salgenuni  43766  issalgend  43767  salgencntex  43772  subsaliuncllem  43786  sge0fodjrnlem  43844  meadjiunlem  43893  caragenel  43923  ovnlecvr  43986  ovnpnfelsup  43987  ovncvrrp  43992  ovnsubaddlem1  43998  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem4  44026  ovnhoilem1  44029  ovnlecvr2  44038  ovncvr2  44039  issmflem  44150  smflimlem2  44194  smflimlem3  44195  smflimsuplem2  44241  elsetpreimafvrab  44734  iccpart  44756  sprel  44824  prelspr  44826  sprsymrelfolem2  44833  sprsymrelf  44835  prpair  44841  paireqne  44851  prprelb  44856  prprelprb  44857  dfodd2  44976  dfeven5  45006  dfodd7  45007  fpprel  45068  1hegrlfgr  45182  ismgmhm  45225  issubmgm  45231  rabsubmgmd  45233  mgmhmeql  45245  assintop  45291  isassintop  45292  assintopcllaw  45294  isrnghm  45338  isrngisom  45342  0even  45377  2even  45379  2zrngamgm  45385  dmatALTbasel  45631  lcoval  45641  elbigo  45785  elrrx2linest2  45979  itsclc0  46005  itsclc0b  46006  itscnhlinecirc02p  46019  unilbss  46051  secval  46335  cscval  46336  cotval  46337