Theorem elrab 3708

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {crab 3443  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490

This theorem is referenced by:  elrab3  3709  elrabd  3710  elrab2  3711  ralrab  3715  rexrab  3718  reurab  3723  rabsnt  4756  unimax  4968  ssintub  4990  intminss  4998  rabxfrd  5435  ssimaex  7007  weniso  7390  canth  7401  riotarab  7447  sorpsscmpl  7769  onnminsb  7835  dfom2  7905  ssnlim  7923  elsuppfng  8210  elsuppfn  8211  ressuppssdif  8226  oeeulem  8657  cofonr  8730  elpmg  8901  fineqvlem  9325  mapfienlem2  9475  supub  9528  suplub  9529  ordtypelem6  9592  ordtypelem7  9593  hartogslem1  9611  hartogs  9613  wemapsolem  9619  card2on  9623  elharval  9630  wdom2d  9649  cantnfs  9735  scottex  9954  tskwe  10019  cardid2  10022  iscard2  10045  cardmin2  10068  acni3  10116  alephsuc2  10149  kmlem1  10220  cofsmo  10338  coftr  10342  fin23lem11  10386  enfin2i  10390  fin1a2lem9  10477  fin1a2lem11  10479  axcc4  10508  axdc3lem2  10520  zorn2lem7  10571  ondomon  10632  alephval2  10641  grutsk  10891  negf1o  11720  infm3  12254  nnind  12311  peano2uz2  12731  peano5uzi  12732  dfuzi  12734  uzind  12735  uzind3  12737  eluz1  12907  uzind4  12971  nnwos  12980  eqreznegel  12999  zmin  13009  elixx1  13416  elioo2  13448  elfz1  13572  flval3  13866  serge0  14107  expge0  14149  expge1  14150  hashbclem  14501  pr2pwpr  14528  elss2prb  14537  hash2sspr  14538  wrdmap  14594  wwlktovfo  15007  shftf  15128  rlimrege0  15625  incexc2  15886  dvdsdivcl  16364  divalglem4  16444  divalgmod  16454  bitsval  16470  bezout  16590  dfgcd2  16593  lcmledvds  16646  lcmgcdlem  16653  lcmfledvds  16679  1nprm  16726  1idssfct  16727  isprm2  16729  hashdvds  16822  phisum  16837  odzval  16838  odzcllem  16839  odzdvds  16842  prmreclem2  16964  prmreclem5  16967  rami  17062  ramub1lem1  17073  ramub1lem2  17074  prmgaplem3  17100  prmgaplem4  17101  prmgaplem5  17102  prmgaplem6  17103  ismre  17648  ismri  17689  isacs  17709  isacs1i  17715  catlid  17741  catrid  17742  ismon  17794  isnat  18015  eldmcoa  18132  fncnvimaeqv  18188  lubeldm  18423  glbeldm  18436  gsumval2  18724  ismgmhm  18734  issubmgm  18740  rabsubmgmd  18742  mgmhmeql  18754  ismhm  18820  issubm  18838  issubmd  18841  mndind  18863  grplinv  19029  issubg  19166  isnsg  19195  cycsubg  19248  isgim  19302  isga  19331  elcntz  19362  elcntzsn  19365  symgfix2  19458  symgsssg  19509  symgfisg  19510  psgnunilem5  19536  odid  19580  odlem2  19581  gexid  19623  gexlem2  19624  gexdvds  19626  isslw  19650  pgpssslw  19656  pj1id  19741  oddvdssubg  19897  pgpfac1lem5  20123  ablfaclem2  20130  isirred  20445  isrnghm  20467  isrngim  20471  isrim0OLD  20507  isrim0  20509  issubrng  20573  issubrg  20599  issdrg  20811  isabv  20834  islss  20955  islmhm  21049  islmim  21084  islbs  21098  psgndiflemB  21641  elocv  21709  isobs  21763  dsmmelbas  21782  frlmelbas  21799  islinds  21852  gsumbagdiaglem  21973  rhmpsrlem2  21984  psrlidm  22005  psrridm  22006  psrass1  22007  psrcom  22011  mplsubglem  22042  mpllsslem  22043  evlsval2  22134  ismhp  22167  ismhp3  22169  mhpmulcl  22176  psdmul  22193  coe1ae0  22239  coe1mul2  22293  dmatel  22520  scmatel  22532  scmateALT  22539  symgmatr01lem  22680  pmatcoe1fsupp  22728  cpmatel  22738  chpscmat  22869  istopon  22939  fctop  23032  cctop  23034  ppttop  23035  pptbas  23036  epttop  23037  iscld  23056  clscld  23076  isnei  23132  neips  23142  neiptopnei  23161  iscn  23264  iscnp  23266  cmpsublem  23428  conncompconn  23461  2ndc1stc  23480  2ndcdisj  23485  elkgen  23565  xkoccn  23648  txdis1cn  23664  txkgen  23681  xkococnlem  23688  xkococn  23689  xkoinjcn  23716  txconn  23718  elqtop  23726  elmptrab  23856  fbssfi  23866  opnfbas  23871  elfg  23900  cfinfil  23922  csdfil  23923  supfil  23924  filssufilg  23940  uffix  23950  fixufil  23951  uffixfr  23952  elflim2  23993  fclscf  24054  flimfnfcls  24057  alexsubALTlem2  24077  alexsubALTlem4  24079  alexsubALT  24080  ptcmplem2  24082  elutop  24263  isucn  24308  iscfilu  24318  ispsmet  24335  ismet  24354  isxmet  24355  elblps  24418  elbl  24419  restmetu  24604  icccmp  24866  elcncf  24934  ishtpy  25023  isphtpy  25032  om1elbas  25084  iscfil  25318  iscau  25329  iscmet  25337  lmle  25354  rrxfsupp  25455  minveclem3  25482  minveclem4  25485  ovolshftlem1  25563  ovolscalem1  25567  ovolicc2lem3  25573  dyadmax  25652  dyadmbllem  25653  opnmbllem  25655  vitalilem2  25663  vitalilem3  25664  elcpn  25990  ig1pval3  26237  coelem  26285  quotlem  26360  elqaalem1  26379  elqaalem3  26381  aannenlem1  26388  aannenlem2  26389  dmarea  27018  jensen  27050  ftalem4  27137  efnnfsumcl  27164  efchtdvds  27220  sqff1o  27243  fsumdvdsdiaglem  27244  dvdsppwf1o  27247  dvdsflf1o  27248  dvdsflsumcom  27249  musum  27252  muinv  27254  logfac2  27279  dchrelbas  27298  lgsfle1  27368  lgsle1  27374  lgsdirprm  27393  lgsne0  27397  lgsquadlem1  27442  lgsquadlem2  27443  dchrvmasumlem1  27557  logsqvma  27604  pntleml  27673  sltval2  27719  sltres  27725  conway  27862  scutcut  27864  scutbday  27867  scutun12  27873  scutbdaybnd2  27879  scutbdaylt  27881  bday1s  27894  cutlt  27984  precsexlem8  28256  precsexlem9  28257  precsexlem11  28259  noseqinds  28317  peano5uzs  28408  uzsind  28409  tgellng  28579  mircgr  28683  mirbtwn  28684  iseqlg  28893  ttgelitv  28915  upgrle  29125  upgrbi  29128  umgredg2  29135  umgrbi  29136  edgupgr  29169  edgumgr  29170  upgredg  29172  numedglnl  29179  edgusgr  29195  usgruspgrb  29218  usgredg2ALT  29228  ushgredgedg  29264  ushgredgedgloop  29266  usgrexmplef  29294  upgrreslem  29339  umgrreslem  29340  upgrres1  29348  nbgrel  29375  nbupgrel  29380  nbumgrvtx  29381  nbusgreledg  29388  nbgrnself  29394  uvtxusgrel  29438  vtxdgoddnumeven  29589  rgrusgrprc  29625  lfgrwlkprop  29723  iswwlks  29869  iswwlksn  29871  wwlksnextsurj  29933  rusgrnumwwlkslem  30002  rusgrnumwwlks  30007  isclwwlk  30016  clwwlknscsh  30094  eleclclwwlkn  30108  clwlknf1oclwwlkn  30116  clwwlkvbij  30145  eupth2lems  30270  konigsberglem4  30287  fusgreg2wsplem  30365  2clwwlkel  30381  extwwlkfabel  30385  clwwlknonclwlknonf1o  30394  dlwwlknondlwlknonf1o  30397  numclwwlk2lem1  30408  numclwlk2lem2f  30409  numclwlk2lem2f1o  30411  grpoidinv2  30547  grpoinv  30557  isssp  30756  islno  30785  isblo  30814  ishmo  30843  ubthlem1  30902  ubthlem2  30903  htthlem  30949  ocel  31313  shsval2i  31419  ococin  31440  chsupsn  31445  eleigvec  31989  cnlnadjlem5  32103  shatomistici  32393  hatomistici  32394  dmrab  32525  nnindf  32823  ismnt  32956  pwrssmgc  32973  tocycf  33110  tocyc01  33111  trsp2cyc  33116  cycpmco2f1  33117  cycpmco2rn  33118  cycpmco2lem2  33120  cycpmco2lem3  33121  cycpmco2lem5  33123  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmconjv  33135  tocyccntz  33137  cyc3evpm  33143  cycpmgcl  33146  cycpmconjslem2  33148  cyc3conja  33150  fldgensdrg  33281  nsgmgclem  33404  nsgmgc  33405  nsgqusf1olem2  33407  isprmidl  33431  ismxidl  33455  ssmxidl  33467  isrprm  33510  1arithufdlem3  33539  1arithufdlem4  33540  1arithufd  33541  fedgmullem2  33643  ply1annnr  33696  minplyann  33702  minplyirred  33704  constrsuc  33728  zarclsiin  33817  zart0  33825  rhmpreimacnlem  33830  ordtconnlem1  33870  indf1ofs  33990  sigagenval  34104  ldsysgenld  34124  ldgenpisyslem1  34127  ldgenpisyslem2  34128  ldgenpisys  34130  ddemeas  34200  ismbfm  34215  imambfm  34227  dya2iocuni  34248  oms0  34262  omssubadd  34265  elcarsg  34270  issibf  34298  sitgfval  34306  oddpwdc  34319  eulerpartlemgh  34343  eulerpartlemgs2  34345  dstfrvel  34438  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemiex  34466  ballotlemfrcn0  34494  ballotlemirc  34496  ballotlem7  34500  reprsum  34590  reprsuc  34592  reprpmtf1o  34603  reprdifc  34604  fnrelpredd  35065  connpconn  35203  iscvm  35227  cvmsi  35233  cvmsval  35234  cvmliftmolem2  35250  cvmliftiota  35269  snmlval  35299  satfv1lem  35330  fmlafvel  35353  fmla1  35355  fmlaomn0  35358  satfv0fvfmla0  35381  sategoelfvb  35387  elmpst  35504  lineelsb2  36112  linerflx1  36113  fwddifval  36126  fwddifnval  36127  rankeq1o  36135  finminlem  36284  fneint  36314  fnessref  36323  topmeet  36330  topjoin  36331  neifg  36337  weiunlem2  36429  weiunfrlem  36430  weiunse  36434  relowlssretop  37329  fin2solem  37566  fin2so  37567  poimirlem4  37584  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem31  37611  poimirlem32  37612  opnmbllem0  37616  mblfinlem2  37618  itg2gt0cn  37635  indexa  37693  nninfnub  37711  istotbnd  37729  sstotbnd2  37734  isbnd  37740  isrngohom  37925  isrngoiso  37938  isidl  37974  ispridl  37994  ismaxidl  38000  prnc  38027  isfldidl  38028  islshp  38935  lssats  38968  islfl  39016  isat  39242  atlatmstc  39275  islln  39463  islpln  39487  islvol  39530  linepsubN  39709  elpmap  39715  pmapsub  39725  elpadd  39756  paddvaln0N  39758  islhp  39953  isldil  40067  isltrn  40076  isdilN  40111  istrnN  40114  diaval  40989  diaelval  40990  diaeldm  40993  diaelrnN  41002  cdlemm10N  41075  docaclN  41081  dibglbN  41123  dicval  41133  dicfnN  41140  dicvalrelN  41142  dihglblem2aN  41250  dihglblem2N  41251  dihglblem3N  41252  dih1dimatlem  41286  dihglb2  41299  dochvalr  41314  doch2val2  41321  dochocss  41323  islpolN  41440  mapd0  41622  aks4d1p4  42036  aks4d1p7  42040  isprimroot  42050  linvh  42053  primrootsunit1  42054  primrootscoprmpow  42056  primrootscoprbij  42059  sticksstones3  42105  aks6d1c6lem3  42129  grpods  42151  unitscyglem2  42153  unitscyglem4  42155  unitscyglem5  42156  supinf  42237  fsuppssindlem2  42547  infdesc  42598  isnacs  42660  elmzpcl  42682  mzpindd  42702  rencldnfilem  42776  irrapxlem6  42783  pellexlem3  42787  pellexlem5  42789  elpell1qr  42803  elpell14qr  42805  elpell1234qr  42807  pellfundre  42837  pellfundge  42838  pellfundlb  42840  pellfundglb  42841  rmspecnonsq  42863  jm2.22  42952  jm2.23  42953  rpnnen3lem  42988  fnwe2lem2  43008  elmnc  43093  dgraalem  43102  dgraaub  43105  mpaalem  43109  rgspnmin  43128  onsucelab  43225  limnsuc  43227  sqrtcvallem1  43593  rfovcnvf1od  43966  scottelrankd  44216  nzss  44286  iccshift  45436  iooshift  45440  limcperiod  45549  sumnnodd  45551  ioodvbdlimc1lem1  45852  dvnprodlem1  45867  dvnprodlem3  45869  itgperiod  45902  stoweidlem14  45935  stoweidlem15  45936  stoweidlem16  45937  stoweidlem31  45952  stoweidlem36  45957  stoweidlem46  45967  stoweidlem48  45969  fourierdlem2  46030  fourierdlem3  46031  fourierdlem20  46048  fourierdlem25  46053  fourierdlem37  46065  fourierdlem42  46070  fourierdlem48  46075  fourierdlem51  46078  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  fourierdlem79  46106  fourierdlem81  46108  elaa2lem  46154  etransclem24  46179  etransclem26  46181  etransclem28  46183  etransclem35  46190  etransclem48  46203  salgenval  46242  salgenn0  46252  salgencl  46253  sssalgen  46256  salgenss  46257  salgenuni  46258  issalgend  46259  salgencntex  46264  subsaliuncllem  46278  sge0fodjrnlem  46337  meadjiunlem  46386  caragenel  46416  ovnlecvr  46479  ovnpnfelsup  46480  ovncvrrp  46485  ovnsubaddlem1  46491  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem4  46519  ovnhoilem1  46522  ovnlecvr2  46531  ovncvr2  46532  issmflem  46648  smflimlem2  46693  smflimlem3  46694  smflimsuplem2  46742  elsetpreimafvrab  47268  iccpart  47290  sprel  47358  prelspr  47360  sprsymrelfolem2  47367  sprsymrelf  47369  prpair  47375  paireqne  47385  prprelb  47390  prprelprb  47391  dfodd2  47510  dfeven5  47540  dfodd7  47541  fpprel  47602  clnbgrel  47701  clnbupgrel  47707  sclnbgrel  47719  vopnbgrel  47726  dfclnbgr6  47728  dfnbgr6  47729  uhgrimisgrgric  47783  grtriprop  47792  isgrtri  47794  uspgrlimlem3  47814  uspgrlim  47816  grlimgrtrilem1  47818  grlimgrtrilem2  47819  1hegrlfgr  47855  assintop  47932  isassintop  47933  assintopcllaw  47935  0even  47960  2even  47962  2zrngamgm  47968  dmatALTbasel  48131  lcoval  48141  elbigo  48285  elrrx2linest2  48479  itsclc0  48505  itsclc0b  48506  itscnhlinecirc02p  48519  unilbss  48549  secval  48839  cscval  48840  cotval  48841