Theorem elrab 3650

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142  {crab 3414  Vcvv 3454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456

This theorem is referenced by:  elrab3  3651  elrabd  3652  elrabrd  3653  elrab2  3654  ralrab  3657  rexrab  3659  reurab  3664  rabsnt  4690  unimax  4903  ssintub  4924  intminss  4932  rabxfrd  5374  ssimaex  6952  weniso  7338  canth  7350  riotarab  7395  sorpsscmpl  7717  onnminsb  7782  dfom2  7848  ssnlim  7866  elsuppfng  8149  elsuppfn  8150  ressuppssdif  8165  oeeulem  8571  cofonr  8644  elpmg  8824  fineqvlem  9210  mapfienlem2  9352  supub  9405  suplub  9406  ordtypelem6  9471  ordtypelem7  9472  hartogslem1  9490  hartogs  9492  wemapsolem  9498  card2on  9502  elharval  9509  wdom2d  9528  cantnfs  9621  scottex  9843  tskwe  9908  cardid2  9911  iscard2  9934  cardmin2  9957  acni3  10003  alephsuc2  10036  kmlem1  10107  cofsmo  10226  coftr  10230  fin23lem11  10274  enfin2i  10278  fin1a2lem9  10365  fin1a2lem11  10367  axcc4  10396  axdc3lem2  10408  zorn2lem7  10459  ondomon  10520  alephval2  10530  grutsk  10780  negf1o  11617  infm3  12151  nnind  12228  peano2uz2  12661  peano5uzi  12662  dfuzi  12664  uzind  12665  uzind3  12667  eluz1  12843  uzind4  12907  nnwos  12916  eqreznegel  12935  zmin  12945  elixx1  13358  elioo2  13390  elfz1  13517  flval3  13825  serge0  14069  expge0  14111  expge1  14112  hashbclem  14465  pr2pwpr  14492  elss2prb  14501  hash2sspr  14502  wrdmap  14559  wwlktovfo  14971  shftf  15092  rlimrege0  15606  incexc2  15868  dvdsdivcl  16350  divalglem4  16430  divalgmod  16440  bitsval  16458  bezout  16577  dfgcd2  16580  lcmledvds  16633  lcmgcdlem  16640  lcmfledvds  16666  1nprm  16713  1idssfct  16714  isprm2  16716  hashdvds  16810  phisum  16826  odzval  16827  odzcllem  16828  odzdvds  16831  prmreclem2  16953  prmreclem5  16956  rami  17051  ramub1lem1  17062  ramub1lem2  17063  prmgaplem3  17089  prmgaplem4  17090  prmgaplem5  17091  prmgaplem6  17092  ismre  17618  ismri  17663  isacs  17683  isacs1i  17689  catlid  17715  catrid  17716  ismon  17766  isnat  17983  eldmcoa  18098  fncnvimaeqv  18152  lubeldm  18383  glbeldm  18396  gsumval2  18720  ismgmhm  18730  issubmgm  18736  rabsubmgmd  18738  mgmhmeql  18750  ismhm  18819  issubm  18837  issubmd  18840  mndind  18862  grplinv  19031  issubg  19168  isnsg  19196  cycsubg  19249  isgim  19302  isga  19331  elcntz  19362  elcntzsn  19365  symgfix2  19456  symgsssg  19507  symgfisg  19508  psgnunilem5  19534  odid  19578  odlem2  19579  gexid  19621  gexlem2  19622  gexdvds  19624  isslw  19648  pgpssslw  19654  pj1id  19739  oddvdssubg  19895  pgpfac1lem5  20121  ablfaclem2  20128  isirred  20464  isrnghm  20486  isrngim  20490  isrim0  20527  issubrng  20593  issubrg  20617  rgspnmin  20661  issdrg  20834  isabv  20857  islss  20998  islmhm  21091  islmim  21126  islbs  21140  psgndiflemB  21649  elocv  21717  isobs  21769  dsmmelbas  21788  frlmelbas  21805  islinds  21858  gsumbagdiaglem  21980  rhmpsrlem2  21990  psrlidm  22010  psrridm  22011  psrass1  22012  psrcom  22016  mplsubglem  22047  mpllsslem  22048  evlsval2  22137  ismhp  22202  ismhp3  22204  mhpmulcl  22211  psdmul  22228  coe1ae0  22275  coe1mul2  22329  dmatel  22550  scmatel  22562  scmateALT  22569  symgmatr01lem  22710  pmatcoe1fsupp  22758  cpmatel  22768  chpscmat  22899  istopon  22969  fctop  23061  cctop  23063  ppttop  23064  pptbas  23065  epttop  23066  iscld  23084  clscld  23104  isnei  23160  neips  23170  neiptopnei  23189  iscn  23292  iscnp  23294  cmpsublem  23456  conncompconn  23489  2ndc1stc  23508  2ndcdisj  23513  elkgen  23593  xkoccn  23676  txdis1cn  23692  txkgen  23709  xkococnlem  23716  xkococn  23717  xkoinjcn  23744  txconn  23746  elqtop  23754  elmptrab  23884  fbssfi  23894  opnfbas  23899  elfg  23928  cfinfil  23950  csdfil  23951  supfil  23952  filssufilg  23968  uffix  23978  fixufil  23979  uffixfr  23980  elflim2  24021  fclscf  24082  flimfnfcls  24085  alexsubALTlem2  24105  alexsubALTlem4  24107  alexsubALT  24108  ptcmplem2  24110  elutop  24290  isucn  24334  iscfilu  24344  ispsmet  24361  ismet  24380  isxmet  24381  elblps  24444  elbl  24445  restmetu  24627  icccmp  24883  elcncf  24948  ishtpy  25031  isphtpy  25040  om1elbas  25091  iscfil  25324  iscau  25335  iscmet  25343  lmle  25360  rrxfsupp  25461  minveclem3  25488  minveclem4  25491  ovolshftlem1  25568  ovolscalem1  25572  ovolicc2lem3  25578  dyadmax  25657  dyadmbllem  25658  opnmbllem  25660  vitalilem2  25668  vitalilem3  25669  elcpn  25993  ig1pval3  26235  coelem  26283  quotlem  26361  elqaalem1  26380  elqaalem3  26382  aannenlem1  26389  aannenlem2  26390  dmarea  27019  jensen  27050  ftalem4  27137  efnnfsumcl  27164  efchtdvds  27220  sqff1o  27243  fsumdvdsdiaglem  27244  dvdsppwf1o  27247  dvdsflf1o  27248  dvdsflsumcom  27249  musum  27252  muinv  27254  logfac2  27278  dchrelbas  27297  lgsfle1  27367  lgsle1  27373  lgsdirprm  27392  lgsne0  27396  lgsquadlem1  27441  lgsquadlem2  27442  dchrvmasumlem1  27556  logsqvma  27603  pntleml  27672  ltsval2  27717  ltsres  27723  conway  27869  cutcuts  27871  cutbday  27874  cutsun12  27880  cutbdaybnd2  27886  cutbdaylt  27888  bday1  27904  cutlt  28022  precsexlem8  28304  precsexlem9  28305  precsexlem11  28307  oncutlt  28354  noseqinds  28383  peano5uzs  28494  uzsind  28495  tgellng  28719  mircgr  28827  mirbtwn  28828  elplng  28984  iseqlg  29058  ttgelitv  29080  upgrle  29288  upgrbi  29291  umgredg2  29298  umgrbi  29299  edgupgr  29332  edgumgr  29333  upgredg  29335  numedglnl  29342  edgusgr  29358  usgruspgrb  29381  usgredg2ALT  29391  ushgredgedg  29427  ushgredgedgloop  29429  usgrexmplef  29457  upgrreslem  29502  umgrreslem  29503  upgrres1  29511  nbgrel  29538  nbupgrel  29543  nbumgrvtx  29544  nbusgreledg  29551  nbgrnself  29557  uvtxusgrel  29601  vtxdgoddnumeven  29751  rgrusgrprc  29787  lfgrwlkprop  29883  iswwlks  30033  iswwlksn  30035  wwlksnextsurj  30097  rusgrnumwwlkslem  30169  rusgrnumwwlks  30174  isclwwlk  30183  clwwlknscsh  30261  eleclclwwlkn  30275  clwlknf1oclwwlkn  30283  clwwlkvbij  30312  eupth2lems  30437  konigsberglem4  30454  fusgreg2wsplem  30532  2clwwlkel  30548  extwwlkfabel  30552  clwwlknonclwlknonf1o  30561  dlwwlknondlwlknonf1o  30564  numclwwlk2lem1  30575  numclwlk2lem2f  30576  numclwlk2lem2f1o  30578  grpoidinv2  30715  grpoinv  30725  isssp  30924  islno  30953  isblo  30982  ishmo  31011  ubthlem1  31070  ubthlem2  31071  htthlem  31117  ocel  31481  shsval2i  31587  ococin  31608  chsupsn  31613  eleigvec  32157  cnlnadjlem5  32271  shatomistici  32561  hatomistici  32562  dmrab  32693  nnindf  33019  indf1ofs  33041  ismnt  33158  pwrssmgc  33175  tocycf  33294  tocyc01  33295  trsp2cyc  33300  cycpmco2f1  33301  cycpmco2rn  33302  cycpmco2lem2  33304  cycpmco2lem3  33305  cycpmco2lem5  33307  cycpmco2lem6  33308  cycpmco2lem7  33309  cycpmconjv  33319  tocyccntz  33321  cyc3evpm  33327  cycpmgcl  33330  cyc3conja  33334  isfxp  33345  fxpgaeq  33346  elrgspnsubrun  33427  rlocisunit  33454  fldgensdrg  33498  nsgmgclem  33594  nsgmgc  33595  nsgqusf1olem2  33597  isprmidl  33621  ismxidl  33647  ssmxidl  33659  isrprm  33710  1arithufdlem3  33739  1arithufdlem4  33740  1arithufd  33741  mplvrpmlem  33837  mplvrpmga  33839  mplvrpmmhm  33840  fedgmullem2  33924  ply1annnr  33997  minplyann  34003  minplyirred  34005  constrsuc  34032  zarclsiin  34165  zart0  34173  rhmpreimacnlem  34178  ordtconnlem1  34218  sigagenval  34434  ldsysgenld  34454  ldgenpisyslem1  34457  ldgenpisyslem2  34458  ldgenpisys  34460  ddemeas  34530  ismbfm  34545  imambfm  34556  dya2iocuni  34577  oms0  34591  omssubadd  34594  elcarsg  34599  issibf  34627  sitgfval  34635  oddpwdc  34648  eulerpartlemgh  34672  eulerpartlemgs2  34674  dstfrvel  34768  ballotlemfc0  34787  ballotlemfcc  34788  ballotlemiex  34796  ballotlemfrcn0  34824  ballotlemirc  34826  ballotlem7  34830  reprsum  34904  reprsuc  34906  reprpmtf1o  34917  reprdifc  34918  fnrelpredd  35384  fineqvnttrclselem2  35415  connpconn  35582  iscvm  35606  cvmsi  35612  cvmsval  35613  cvmliftmolem2  35629  cvmliftiota  35648  snmlval  35678  satfv1lem  35709  fmlafvel  35732  fmla1  35734  fmlaomn0  35737  satfv0fvfmla0  35760  sategoelfvb  35766  elmpst  35883  lineelsb2  36495  linerflx1  36496  fwddifval  36509  fwddifnval  36510  rankeq1o  36518  finminlem  36675  fneint  36705  fnessref  36714  topmeet  36721  topjoin  36722  neifg  36728  weiunlem  36820  weiunfrlem  36821  weiunse  36825  regsfromregtco  36895  relowlssretop  37854  fin2solem  38102  fin2so  38103  poimirlem4  38120  poimirlem25  38141  poimirlem26  38142  poimirlem27  38143  poimirlem31  38147  poimirlem32  38148  opnmbllem0  38152  mblfinlem2  38154  itg2gt0cn  38171  indexa  38229  nninfnub  38247  istotbnd  38265  sstotbnd2  38270  isbnd  38276  isrngohom  38461  isrngoiso  38474  isidl  38510  ispridl  38530  ismaxidl  38536  prnc  38563  isfldidl  38564  islshp  39600  lssats  39633  islfl  39681  isat  39907  atlatmstc  39940  islln  40127  islpln  40151  islvol  40194  linepsubN  40373  elpmap  40379  pmapsub  40389  elpadd  40420  paddvaln0N  40422  islhp  40617  isldil  40731  isltrn  40740  isdilN  40775  istrnN  40778  diaval  41653  diaelval  41654  diaeldm  41657  diaelrnN  41666  cdlemm10N  41739  docaclN  41745  dibglbN  41787  dicval  41797  dicfnN  41804  dicvalrelN  41806  dihglblem2aN  41914  dihglblem2N  41915  dihglblem3N  41916  dih1dimatlem  41950  dihglb2  41963  dochvalr  41978  doch2val2  41985  dochocss  41987  islpolN  42104  mapd0  42286  aks4d1p4  42693  aks4d1p7  42697  isprimroot  42707  linvh  42710  primrootsunit1  42711  primrootscoprmpow  42713  primrootscoprbij  42716  sticksstones3  42762  aks6d1c6lem3  42786  grpods  42808  unitscyglem2  42810  unitscyglem4  42812  unitscyglem5  42813  supinf  42855  fsuppssindlem2  43171  infdesc  43222  isnacs  43282  elmzpcl  43304  mzpindd  43324  rencldnfilem  43394  irrapxlem6  43401  pellexlem3  43405  pellexlem5  43407  elpell1qr  43421  elpell14qr  43423  elpell1234qr  43425  pellfundre  43455  pellfundge  43456  pellfundlb  43458  pellfundglb  43459  rmspecnonsq  43481  jm2.22  43569  jm2.23  43570  rpnnen3lem  43605  fnwe2lem2  43625  elmnc  43710  dgraalem  43719  dgraaub  43722  mpaalem  43726  onsucelab  43837  limnsuc  43839  sqrtcvallem1  44204  rfovcnvf1od  44577  scottelrankd  44820  nzss  44890  iccshift  46091  iooshift  46095  limcperiod  46201  sumnnodd  46203  ioodvbdlimc1lem1  46502  dvnprodlem1  46517  dvnprodlem3  46519  itgperiod  46552  stoweidlem14  46585  stoweidlem15  46586  stoweidlem16  46587  stoweidlem31  46602  stoweidlem36  46607  stoweidlem46  46617  stoweidlem48  46619  fourierdlem2  46680  fourierdlem3  46681  fourierdlem20  46698  fourierdlem25  46703  fourierdlem37  46715  fourierdlem42  46720  fourierdlem48  46725  fourierdlem51  46728  fourierdlem63  46740  fourierdlem64  46741  fourierdlem65  46742  fourierdlem79  46756  fourierdlem81  46758  elaa2lem  46804  etransclem24  46829  etransclem26  46831  etransclem28  46833  etransclem35  46840  etransclem48  46853  salgenval  46892  salgenn0  46902  salgencl  46903  sssalgen  46906  salgenss  46907  salgenuni  46908  issalgend  46909  salgencntex  46914  subsaliuncllem  46928  sge0fodjrnlem  46987  meadjiunlem  47036  caragenel  47066  ovnlecvr  47129  ovnpnfelsup  47130  ovncvrrp  47135  ovnsubaddlem1  47141  hoidmv1lelem1  47162  hoidmv1lelem2  47163  hoidmv1lelem3  47164  hoidmvlelem1  47166  hoidmvlelem2  47167  hoidmvlelem4  47169  ovnhoilem1  47172  ovnlecvr2  47181  ovncvr2  47182  issmflem  47298  smflimlem2  47343  smflimlem3  47344  smflimsuplem2  47392  elsetpreimafvrab  47997  iccpart  48019  sprel  48087  prelspr  48089  sprsymrelfolem2  48096  sprsymrelf  48098  prpair  48104  paireqne  48114  prprelb  48119  prprelprb  48120  dfodd2  48255  dfeven5  48285  dfodd7  48286  fpprel  48347  clnbgrel  48447  clnbupgrel  48453  sclnbgrel  48466  vopnbgrel  48473  dfclnbgr6  48475  dfnbgr6  48476  isubgredg  48485  uhgrimisgrgric  48550  grtriprop  48560  isgrtri  48562  stgredgel  48576  stgrusgra  48578  uspgrlimlem3  48609  uspgrlim  48611  grlimgredgex  48619  grlimgrtrilem2  48621  gpgiedgdmel  48668  gpgedgel  48669  gpgnbgrvtx0  48693  gpgnbgrvtx1  48694  gpgprismgr4cycllem10  48723  1hegrlfgr  48751  assintop  48828  isassintop  48829  assintopcllaw  48831  0even  48856  2even  48858  2zrngamgm  48864  dmatALTbasel  49021  lcoval  49031  elbigo  49170  elrrx2linest2  49364  itsclc0  49390  itsclc0b  49391  itscnhlinecirc02p  49404  unilbss  49436  secval  50365  cscval  50366  cotval  50367