Theorem elrab 3648

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {crab 3405  Vcvv 3446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448

This theorem is referenced by:  elrab3  3649  elrabd  3650  elrab2  3651  ralrab  3654  rexrab  3657  reurab  3662  rabsnt  4697  unimax  4910  ssintub  4932  intminss  4940  rabxfrd  5377  ssimaex  6931  weniso  7304  canth  7315  riotarab  7361  sorpsscmpl  7676  onnminsb  7739  dfom2  7809  ssnlim  7827  elsuppfng  8106  elsuppfn  8107  ressuppssdif  8121  oeeulem  8553  cofonr  8625  elpmg  8788  fineqvlem  9213  mapfienlem2  9351  supub  9404  suplub  9405  ordtypelem6  9468  ordtypelem7  9469  hartogslem1  9487  hartogs  9489  wemapsolem  9495  card2on  9499  elharval  9506  wdom2d  9525  cantnfs  9611  scottex  9830  tskwe  9895  cardid2  9898  iscard2  9921  cardmin2  9944  acni3  9992  alephsuc2  10025  kmlem1  10095  cofsmo  10214  coftr  10218  fin23lem11  10262  enfin2i  10266  fin1a2lem9  10353  fin1a2lem11  10355  axcc4  10384  axdc3lem2  10396  zorn2lem7  10447  ondomon  10508  alephval2  10517  grutsk  10767  negf1o  11594  infm3  12123  nnind  12180  peano2uz2  12600  peano5uzi  12601  dfuzi  12603  uzind  12604  uzind3  12606  eluz1  12776  uzind4  12840  nnwos  12849  eqreznegel  12868  zmin  12878  elixx1  13283  elioo2  13315  elfz1  13439  flval3  13730  serge0  13972  expge0  14014  expge1  14015  hashbclem  14361  pr2pwpr  14390  elss2prb  14398  hash2sspr  14399  wrdmap  14446  wwlktovfo  14859  shftf  14976  rlimrege0  15473  incexc2  15734  dvdsdivcl  16209  divalglem4  16289  divalgmod  16299  bitsval  16315  bezout  16435  dfgcd2  16438  lcmledvds  16486  lcmgcdlem  16493  lcmfledvds  16519  1nprm  16566  1idssfct  16567  isprm2  16569  hashdvds  16658  phisum  16673  odzval  16674  odzcllem  16675  odzdvds  16678  prmreclem2  16800  prmreclem5  16803  rami  16898  ramub1lem1  16909  ramub1lem2  16910  prmgaplem3  16936  prmgaplem4  16937  prmgaplem5  16938  prmgaplem6  16939  ismre  17484  ismri  17525  isacs  17545  isacs1i  17551  catlid  17577  catrid  17578  ismon  17630  isnat  17848  eldmcoa  17965  fncnvimaeqv  18021  lubeldm  18256  glbeldm  18269  gsumval2  18555  ismhm  18617  issubm  18628  issubmd  18631  mndind  18652  grplinv  18814  issubg  18942  isnsg  18971  cycsubg  19015  isgim  19066  isga  19085  elcntz  19116  elcntzsn  19119  symgfix2  19212  symgsssg  19263  symgfisg  19264  psgnunilem5  19290  odid  19334  odlem2  19335  gexid  19377  gexlem2  19378  gexdvds  19380  isslw  19404  pgpssslw  19410  pj1id  19495  oddvdssubg  19647  pgpfac1lem5  19872  ablfaclem2  19879  isirred  20144  isrim0OLD  20170  isrim0  20172  issubrg  20270  issdrg  20311  isabv  20334  islss  20452  islmhm  20545  islmim  20580  islbs  20594  psgndiflemB  21041  elocv  21109  isobs  21163  dsmmelbas  21182  frlmelbas  21199  islinds  21252  gsumbagdiaglemOLD  21377  gsumbagdiaglem  21380  psrmulcllem  21392  psrlidm  21409  psrridm  21410  psrass1  21411  psrcom  21415  mplsubglem  21442  mpllsslem  21443  evlsval2  21534  ismhp  21568  ismhp3  21570  mhpmulcl  21576  coe1ae0  21624  coe1mul2  21677  dmatel  21879  scmatel  21891  scmateALT  21898  symgmatr01lem  22039  pmatcoe1fsupp  22087  cpmatel  22097  chpscmat  22228  istopon  22298  fctop  22391  cctop  22393  ppttop  22394  pptbas  22395  epttop  22396  iscld  22415  clscld  22435  isnei  22491  neips  22501  neiptopnei  22520  iscn  22623  iscnp  22625  cmpsublem  22787  conncompconn  22820  2ndc1stc  22839  2ndcdisj  22844  elkgen  22924  xkoccn  23007  txdis1cn  23023  txkgen  23040  xkococnlem  23047  xkococn  23048  xkoinjcn  23075  txconn  23077  elqtop  23085  elmptrab  23215  fbssfi  23225  opnfbas  23230  elfg  23259  cfinfil  23281  csdfil  23282  supfil  23283  filssufilg  23299  uffix  23309  fixufil  23310  uffixfr  23311  elflim2  23352  fclscf  23413  flimfnfcls  23416  alexsubALTlem2  23436  alexsubALTlem4  23438  alexsubALT  23439  ptcmplem2  23441  elutop  23622  isucn  23667  iscfilu  23677  ispsmet  23694  ismet  23713  isxmet  23714  elblps  23777  elbl  23778  restmetu  23963  icccmp  24225  elcncf  24289  ishtpy  24372  isphtpy  24381  om1elbas  24432  iscfil  24666  iscau  24677  iscmet  24685  lmle  24702  rrxfsupp  24803  minveclem3  24830  minveclem4  24833  ovolshftlem1  24910  ovolscalem1  24914  ovolicc2lem3  24920  dyadmax  24999  dyadmbllem  25000  opnmbllem  25002  vitalilem2  25010  vitalilem3  25011  elcpn  25335  ig1pval3  25576  coelem  25624  quotlem  25697  elqaalem1  25716  elqaalem3  25718  aannenlem1  25725  aannenlem2  25726  dmarea  26344  jensen  26375  ftalem4  26462  efnnfsumcl  26489  efchtdvds  26545  sqff1o  26568  fsumdvdsdiaglem  26569  dvdsppwf1o  26572  dvdsflf1o  26573  dvdsflsumcom  26574  musum  26577  muinv  26579  logfac2  26602  dchrelbas  26621  lgsfle1  26691  lgsle1  26697  lgsdirprm  26716  lgsne0  26720  lgsquadlem1  26765  lgsquadlem2  26766  dchrvmasumlem1  26880  logsqvma  26927  pntleml  26996  sltval2  27041  sltres  27047  conway  27181  scutcut  27183  scutbday  27186  scutun12  27192  scutbdaybnd2  27198  scutbdaylt  27200  bday1s  27213  tgellng  27558  mircgr  27662  mirbtwn  27663  iseqlg  27872  ttgelitv  27894  upgrle  28104  upgrbi  28107  umgredg2  28114  umgrbi  28115  edgupgr  28148  edgumgr  28149  upgredg  28151  numedglnl  28158  edgusgr  28174  usgruspgrb  28195  usgredg2ALT  28204  ushgredgedg  28240  ushgredgedgloop  28242  usgrexmplef  28270  upgrreslem  28315  umgrreslem  28316  upgrres1  28324  nbgrel  28351  nbupgrel  28356  nbumgrvtx  28357  nbusgreledg  28364  nbgrnself  28370  uvtxusgrel  28414  vtxdgoddnumeven  28564  rgrusgrprc  28600  lfgrwlkprop  28698  iswwlks  28844  iswwlksn  28846  wwlksnextsurj  28908  rusgrnumwwlkslem  28977  rusgrnumwwlks  28982  isclwwlk  28991  clwwlknscsh  29069  eleclclwwlkn  29083  clwlknf1oclwwlkn  29091  clwwlkvbij  29120  eupth2lems  29245  konigsberglem4  29262  fusgreg2wsplem  29340  2clwwlkel  29356  extwwlkfabel  29360  clwwlknonclwlknonf1o  29369  dlwwlknondlwlknonf1o  29372  numclwwlk2lem1  29383  numclwlk2lem2f  29384  numclwlk2lem2f1o  29386  grpoidinv2  29520  grpoinv  29530  isssp  29729  islno  29758  isblo  29787  ishmo  29816  ubthlem1  29875  ubthlem2  29876  htthlem  29922  ocel  30286  shsval2i  30392  ococin  30413  chsupsn  30418  eleigvec  30962  cnlnadjlem5  31076  shatomistici  31366  hatomistici  31367  dmrab  31489  nnindf  31785  ismnt  31913  pwrssmgc  31930  tocycf  32036  tocyc01  32037  trsp2cyc  32042  cycpmco2f1  32043  cycpmco2rn  32044  cycpmco2lem2  32046  cycpmco2lem3  32047  cycpmco2lem5  32049  cycpmco2lem6  32050  cycpmco2lem7  32051  cycpmconjv  32061  tocyccntz  32063  cyc3evpm  32069  cycpmgcl  32072  cycpmconjslem2  32074  cyc3conja  32076  fldgensdrg  32152  nsgmgclem  32263  nsgmgc  32264  nsgqusf1olem2  32266  isprmidl  32286  ismxidl  32307  ssmxidl  32315  isrprm  32338  fedgmullem2  32412  zarclsiin  32541  zart0  32549  rhmpreimacnlem  32554  ordtconnlem1  32594  indf1ofs  32714  sigagenval  32828  ldsysgenld  32848  ldgenpisyslem1  32851  ldgenpisyslem2  32852  ldgenpisys  32854  ddemeas  32924  ismbfm  32939  imambfm  32951  dya2iocuni  32972  oms0  32986  omssubadd  32989  elcarsg  32994  issibf  33022  sitgfval  33030  oddpwdc  33043  eulerpartlemgh  33067  eulerpartlemgs2  33069  dstfrvel  33162  ballotlemfc0  33181  ballotlemfcc  33182  ballotlemiex  33190  ballotlemfrcn0  33218  ballotlemirc  33220  ballotlem7  33224  reprsum  33315  reprsuc  33317  reprpmtf1o  33328  reprdifc  33329  fnrelpredd  33782  connpconn  33916  iscvm  33940  cvmsi  33946  cvmsval  33947  cvmliftmolem2  33963  cvmliftiota  33982  snmlval  34012  satfv1lem  34043  fmlafvel  34066  fmla1  34068  fmlaomn0  34071  satfv0fvfmla0  34094  sategoelfvb  34100  elmpst  34217  lineelsb2  34809  linerflx1  34810  fwddifval  34823  fwddifnval  34824  rankeq1o  34832  finminlem  34866  fneint  34896  fnessref  34905  topmeet  34912  topjoin  34913  neifg  34919  relowlssretop  35907  fin2solem  36137  fin2so  36138  poimirlem4  36155  poimirlem25  36176  poimirlem26  36177  poimirlem27  36178  poimirlem31  36182  poimirlem32  36183  opnmbllem0  36187  mblfinlem2  36189  itg2gt0cn  36206  indexa  36265  nninfnub  36283  istotbnd  36301  sstotbnd2  36306  isbnd  36312  isrngohom  36497  isrngoiso  36510  isidl  36546  ispridl  36566  ismaxidl  36572  prnc  36599  isfldidl  36600  islshp  37514  lssats  37547  islfl  37595  isat  37821  atlatmstc  37854  islln  38042  islpln  38066  islvol  38109  linepsubN  38288  elpmap  38294  pmapsub  38304  elpadd  38335  paddvaln0N  38337  islhp  38532  isldil  38646  isltrn  38655  isdilN  38690  istrnN  38693  diaval  39568  diaelval  39569  diaeldm  39572  diaelrnN  39581  cdlemm10N  39654  docaclN  39660  dibglbN  39702  dicval  39712  dicfnN  39719  dicvalrelN  39721  dihglblem2aN  39829  dihglblem2N  39830  dihglblem3N  39831  dih1dimatlem  39865  dihglb2  39878  dochvalr  39893  doch2val2  39900  dochocss  39902  islpolN  40019  mapd0  40201  aks4d1p4  40609  aks4d1p7  40613  sticksstones3  40629  rhmmpllem2  40796  rhmcomulmpl  40798  fsuppssindlem2  40825  infdesc  41039  isnacs  41085  elmzpcl  41107  mzpindd  41127  rencldnfilem  41201  irrapxlem6  41208  pellexlem3  41212  pellexlem5  41214  elpell1qr  41228  elpell14qr  41230  elpell1234qr  41232  pellfundre  41262  pellfundge  41263  pellfundlb  41265  pellfundglb  41266  rmspecnonsq  41288  jm2.22  41377  jm2.23  41378  rpnnen3lem  41413  fnwe2lem2  41436  elmnc  41521  dgraalem  41530  dgraaub  41533  mpaalem  41537  rgspnmin  41556  onsucelab  41656  limnsuc  41658  sqrtcvallem1  42025  rfovcnvf1od  42398  scottelrankd  42649  nzss  42719  iccshift  43876  iooshift  43880  limcperiod  43989  sumnnodd  43991  ioodvbdlimc1lem1  44292  dvnprodlem1  44307  dvnprodlem3  44309  itgperiod  44342  stoweidlem14  44375  stoweidlem15  44376  stoweidlem16  44377  stoweidlem31  44392  stoweidlem36  44397  stoweidlem46  44407  stoweidlem48  44409  fourierdlem2  44470  fourierdlem3  44471  fourierdlem20  44488  fourierdlem25  44493  fourierdlem37  44505  fourierdlem42  44510  fourierdlem48  44515  fourierdlem51  44518  fourierdlem63  44530  fourierdlem64  44531  fourierdlem65  44532  fourierdlem79  44546  fourierdlem81  44548  elaa2lem  44594  etransclem24  44619  etransclem26  44621  etransclem28  44623  etransclem35  44630  etransclem48  44643  salgenval  44682  salgenn0  44692  salgencl  44693  sssalgen  44696  salgenss  44697  salgenuni  44698  issalgend  44699  salgencntex  44704  subsaliuncllem  44718  sge0fodjrnlem  44777  meadjiunlem  44826  caragenel  44856  ovnlecvr  44919  ovnpnfelsup  44920  ovncvrrp  44925  ovnsubaddlem1  44931  hoidmv1lelem1  44952  hoidmv1lelem2  44953  hoidmv1lelem3  44954  hoidmvlelem1  44956  hoidmvlelem2  44957  hoidmvlelem4  44959  ovnhoilem1  44962  ovnlecvr2  44971  ovncvr2  44972  issmflem  45088  smflimlem2  45133  smflimlem3  45134  smflimsuplem2  45182  elsetpreimafvrab  45706  iccpart  45728  sprel  45796  prelspr  45798  sprsymrelfolem2  45805  sprsymrelf  45807  prpair  45813  paireqne  45823  prprelb  45828  prprelprb  45829  dfodd2  45948  dfeven5  45978  dfodd7  45979  fpprel  46040  1hegrlfgr  46154  ismgmhm  46197  issubmgm  46203  rabsubmgmd  46205  mgmhmeql  46217  assintop  46263  isassintop  46264  assintopcllaw  46266  isrnghm  46310  isrngisom  46314  0even  46349  2even  46351  2zrngamgm  46357  dmatALTbasel  46603  lcoval  46613  elbigo  46757  elrrx2linest2  46951  itsclc0  46977  itsclc0b  46978  itscnhlinecirc02p  46991  unilbss  47022  secval  47312  cscval  47313  cotval  47314