Theorem elrab 3628

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {crab 3110  Vcvv 3441

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443

This theorem is referenced by:  elrab3  3629  elrabd  3630  elrab2  3631  ralrab  3633  rexrab  3635  rabsnt  4627  unimax  4836  ssintub  4856  intminss  4864  rabxfrd  5283  ssimaex  6723  weniso  7086  canth  7090  sorpsscmpl  7440  onnminsb  7499  dfom2  7562  ssnlim  7579  elsuppfn  7821  ressuppssdif  7834  oeeulem  8210  elpmg  8405  fineqvlem  8716  mapfienlem2  8853  supub  8907  suplub  8908  ordtypelem6  8971  ordtypelem7  8972  hartogslem1  8990  hartogs  8992  wemapsolem  8998  card2on  9002  elharval  9009  wdom2d  9028  cantnfs  9113  scottex  9298  tskwe  9363  cardid2  9366  iscard2  9389  cardmin2  9412  acni3  9458  alephsuc2  9491  kmlem1  9561  cofsmo  9680  coftr  9684  fin23lem11  9728  enfin2i  9732  fin1a2lem9  9819  fin1a2lem11  9821  axcc4  9850  axdc3lem2  9862  zorn2lem7  9913  ondomon  9974  alephval2  9983  grutsk  10233  negf1o  11059  infm3  11587  nnind  11643  peano2uz2  12058  peano5uzi  12059  dfuzi  12061  uzind  12062  uzind3  12064  eluz1  12235  uzind4  12294  nnwos  12303  eqreznegel  12322  zmin  12332  elixx1  12735  elioo2  12767  elfz1  12890  flval3  13180  serge0  13420  expge0  13461  expge1  13462  hashbclem  13806  pr2pwpr  13833  elss2prb  13841  hash2sspr  13842  wrdmap  13889  wwlktovfo  14313  shftf  14430  rlimrege0  14928  incexc2  15185  dvdsdivcl  15658  divalglem4  15737  divalgmod  15747  bitsval  15763  bezout  15881  dfgcd2  15884  lcmledvds  15933  lcmgcdlem  15940  lcmfledvds  15966  1nprm  16013  1idssfct  16014  isprm2  16016  hashdvds  16102  phisum  16117  odzval  16118  odzcllem  16119  odzdvds  16122  prmreclem2  16243  prmreclem5  16246  rami  16341  ramub1lem1  16352  ramub1lem2  16353  prmgaplem3  16379  prmgaplem4  16380  prmgaplem5  16381  prmgaplem6  16382  ismre  16853  ismri  16894  isacs  16914  isacs1i  16920  catlid  16946  catrid  16947  ismon  16995  isnat  17209  eldmcoa  17317  fncnvimaeqv  17362  lubeldm  17583  glbeldm  17596  gsumval2  17888  ismhm  17950  issubm  17960  issubmd  17963  mndind  17984  grplinv  18144  issubg  18271  isnsg  18299  cycsubg  18343  isgim  18394  isga  18413  elcntz  18444  elcntzsn  18447  symgfix2  18536  symgsssg  18587  symgfisg  18588  psgnunilem5  18614  odid  18658  odlem2  18659  gexid  18698  gexlem2  18699  gexdvds  18701  isslw  18725  pgpssslw  18731  pj1id  18817  oddvdssubg  18968  pgpfac1lem5  19194  ablfaclem2  19201  isirred  19445  isrim0  19471  issubrg  19528  issdrg  19567  isabv  19583  islss  19699  islmhm  19792  islmim  19827  islbs  19841  psgndiflemB  20289  elocv  20357  isobs  20409  dsmmelbas  20428  frlmelbas  20445  islinds  20498  gsumbagdiaglem  20613  psrmulcllem  20625  psrlidm  20641  psrridm  20642  psrass1  20643  psrcom  20647  mplsubglem  20672  mpllsslem  20673  evlsval2  20759  ismhp  20793  mhpvarcl  20798  coe1ae0  20845  coe1mul2  20898  dmatel  21098  scmatel  21110  scmateALT  21117  symgmatr01lem  21258  pmatcoe1fsupp  21306  cpmatel  21316  chpscmat  21447  istopon  21517  fctop  21609  cctop  21611  ppttop  21612  pptbas  21613  epttop  21614  iscld  21632  clscld  21652  isnei  21708  neips  21718  neiptopnei  21737  iscn  21840  iscnp  21842  cmpsublem  22004  conncompconn  22037  2ndc1stc  22056  2ndcdisj  22061  elkgen  22141  xkoccn  22224  txdis1cn  22240  txkgen  22257  xkococnlem  22264  xkococn  22265  xkoinjcn  22292  txconn  22294  elqtop  22302  elmptrab  22432  fbssfi  22442  opnfbas  22447  elfg  22476  cfinfil  22498  csdfil  22499  supfil  22500  filssufilg  22516  uffix  22526  fixufil  22527  uffixfr  22528  elflim2  22569  fclscf  22630  flimfnfcls  22633  alexsubALTlem2  22653  alexsubALTlem4  22655  alexsubALT  22656  ptcmplem2  22658  elutop  22839  isucn  22884  iscfilu  22894  ispsmet  22911  ismet  22930  isxmet  22931  elblps  22994  elbl  22995  restmetu  23177  icccmp  23430  elcncf  23494  ishtpy  23577  isphtpy  23586  om1elbas  23637  iscfil  23869  iscau  23880  iscmet  23888  lmle  23905  rrxfsupp  24006  minveclem3  24033  minveclem4  24036  ovolshftlem1  24113  ovolscalem1  24117  ovolicc2lem3  24123  dyadmax  24202  dyadmbllem  24203  opnmbllem  24205  vitalilem2  24213  vitalilem3  24214  elcpn  24537  ig1pval3  24775  coelem  24823  quotlem  24896  elqaalem1  24915  elqaalem3  24917  aannenlem1  24924  aannenlem2  24925  dmarea  25543  jensen  25574  ftalem4  25661  efnnfsumcl  25688  efchtdvds  25744  sqff1o  25767  fsumdvdsdiaglem  25768  dvdsppwf1o  25771  dvdsflf1o  25772  dvdsflsumcom  25773  musum  25776  muinv  25778  logfac2  25801  dchrelbas  25820  lgsfle1  25890  lgsle1  25896  lgsdirprm  25915  lgsne0  25919  lgsquadlem1  25964  lgsquadlem2  25965  dchrvmasumlem1  26079  logsqvma  26126  pntleml  26195  tgellng  26347  mircgr  26451  mirbtwn  26452  iseqlg  26661  ttgelitv  26677  upgrle  26883  upgrbi  26886  umgredg2  26893  umgrbi  26894  edgupgr  26927  edgumgr  26928  upgredg  26930  numedglnl  26937  edgusgr  26953  usgruspgrb  26974  usgredg2ALT  26983  ushgredgedg  27019  ushgredgedgloop  27021  usgrexmplef  27049  upgrreslem  27094  umgrreslem  27095  upgrres1  27103  nbgrel  27130  nbupgrel  27135  nbumgrvtx  27136  nbusgreledg  27143  nbgrnself  27149  uvtxusgrel  27193  vtxdgoddnumeven  27343  rgrusgrprc  27379  lfgrwlkprop  27477  iswwlks  27622  iswwlksn  27624  wwlksnextsurj  27686  rusgrnumwwlkslem  27755  rusgrnumwwlks  27760  isclwwlk  27769  clwwlknscsh  27847  eleclclwwlkn  27861  clwlknf1oclwwlkn  27869  clwwlkvbij  27898  eupth2lems  28023  konigsberglem4  28040  fusgreg2wsplem  28118  2clwwlkel  28134  extwwlkfabel  28138  clwwlknonclwlknonf1o  28147  dlwwlknondlwlknonf1o  28150  numclwwlk2lem1  28161  numclwlk2lem2f  28162  numclwlk2lem2f1o  28164  grpoidinv2  28298  grpoinv  28308  isssp  28507  islno  28536  isblo  28565  ishmo  28594  ubthlem1  28653  ubthlem2  28654  htthlem  28700  ocel  29064  shsval2i  29170  ococin  29191  chsupsn  29196  eleigvec  29740  cnlnadjlem5  29854  shatomistici  30144  hatomistici  30145  dmrab  30267  nnindf  30561  ismnt  30691  pwrssmgc  30706  tocycf  30809  tocyc01  30810  trsp2cyc  30815  cycpmco2f1  30816  cycpmco2rn  30817  cycpmco2lem2  30819  cycpmco2lem3  30820  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmconjv  30834  tocyccntz  30836  cyc3evpm  30842  cycpmgcl  30845  cycpmconjslem2  30847  cyc3conja  30849  isprmidl  31021  ismxidl  31042  ssmxidl  31050  isrprm  31073  fedgmullem2  31114  zarclsiin  31224  zart0  31232  rhmpreimacnlem  31237  ordtconnlem1  31277  indf1ofs  31395  sigagenval  31509  ldsysgenld  31529  ldgenpisyslem1  31532  ldgenpisyslem2  31533  ldgenpisys  31535  ddemeas  31605  ismbfm  31620  imambfm  31630  dya2iocuni  31651  oms0  31665  omssubadd  31668  elcarsg  31673  issibf  31701  sitgfval  31709  oddpwdc  31722  eulerpartlemgh  31746  eulerpartlemgs2  31748  dstfrvel  31841  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemiex  31869  ballotlemfrcn0  31897  ballotlemirc  31899  ballotlem7  31903  reprsum  31994  reprsuc  31996  reprpmtf1o  32007  reprdifc  32008  fnrelpredd  32472  connpconn  32595  iscvm  32619  cvmsi  32625  cvmsval  32626  cvmliftmolem2  32642  cvmliftiota  32661  snmlval  32691  satfv1lem  32722  fmlafvel  32745  fmla1  32747  fmlaomn0  32750  satfv0fvfmla0  32773  sategoelfvb  32779  elmpst  32896  sltval2  33276  sltres  33282  conway  33377  scutcut  33379  scutbday  33380  scutun12  33384  scutbdaybnd  33388  scutbdaylt  33389  lineelsb2  33722  linerflx1  33723  fwddifval  33736  fwddifnval  33737  rankeq1o  33745  finminlem  33779  fneint  33809  fnessref  33818  topmeet  33825  topjoin  33826  neifg  33832  relowlssretop  34780  fin2solem  35043  fin2so  35044  poimirlem4  35061  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem31  35088  poimirlem32  35089  opnmbllem0  35093  mblfinlem2  35095  itg2gt0cn  35112  indexa  35171  nninfnub  35189  istotbnd  35207  sstotbnd2  35212  isbnd  35218  isrngohom  35403  isrngoiso  35416  isidl  35452  ispridl  35472  ismaxidl  35478  prnc  35505  isfldidl  35506  islshp  36275  lssats  36308  islfl  36356  isat  36582  atlatmstc  36615  islln  36802  islpln  36826  islvol  36869  linepsubN  37048  elpmap  37054  pmapsub  37064  elpadd  37095  paddvaln0N  37097  islhp  37292  isldil  37406  isltrn  37415  isdilN  37450  istrnN  37453  diaval  38328  diaelval  38329  diaeldm  38332  diaelrnN  38341  cdlemm10N  38414  docaclN  38420  dibglbN  38462  dicval  38472  dicfnN  38479  dicvalrelN  38481  dihglblem2aN  38589  dihglblem2N  38590  dihglblem3N  38591  dih1dimatlem  38625  dihglb2  38638  dochvalr  38653  doch2val2  38660  dochocss  38662  islpolN  38779  mapd0  38961  fsuppssindlem2  39458  isnacs  39645  elmzpcl  39667  mzpindd  39687  rencldnfilem  39761  irrapxlem6  39768  pellexlem3  39772  pellexlem5  39774  elpell1qr  39788  elpell14qr  39790  elpell1234qr  39792  pellfundre  39822  pellfundge  39823  pellfundlb  39825  pellfundglb  39826  rmspecnonsq  39848  jm2.22  39936  jm2.23  39937  rpnnen3lem  39972  fnwe2lem2  39995  elmnc  40080  dgraalem  40089  dgraaub  40092  mpaalem  40096  rgspnmin  40115  sqrtcvallem1  40331  rfovcnvf1od  40705  scottelrankd  40955  nzss  41021  iccshift  42155  iooshift  42159  limcperiod  42270  sumnnodd  42272  ioodvbdlimc1lem1  42573  dvnprodlem1  42588  dvnprodlem3  42590  itgperiod  42623  stoweidlem14  42656  stoweidlem15  42657  stoweidlem16  42658  stoweidlem31  42673  stoweidlem36  42678  stoweidlem46  42688  stoweidlem48  42690  fourierdlem2  42751  fourierdlem3  42752  fourierdlem20  42769  fourierdlem25  42774  fourierdlem37  42786  fourierdlem42  42791  fourierdlem48  42796  fourierdlem51  42799  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  fourierdlem79  42827  fourierdlem81  42829  elaa2lem  42875  etransclem24  42900  etransclem26  42902  etransclem28  42904  etransclem35  42911  etransclem48  42924  salgenval  42963  salgenn0  42971  salgencl  42972  sssalgen  42975  salgenss  42976  salgenuni  42977  issalgend  42978  salgencntex  42983  subsaliuncllem  42997  sge0fodjrnlem  43055  meadjiunlem  43104  caragenel  43134  ovnlecvr  43197  ovnpnfelsup  43198  ovncvrrp  43203  ovnsubaddlem1  43209  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1lelem3  43232  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem4  43237  ovnhoilem1  43240  ovnlecvr2  43249  ovncvr2  43250  issmflem  43361  smflimlem2  43405  smflimlem3  43406  smflimsuplem2  43452  elsetpreimafvrab  43911  iccpart  43933  sprel  44001  prelspr  44003  sprsymrelfolem2  44010  sprsymrelf  44012  prpair  44018  paireqne  44028  prprelb  44033  prprelprb  44034  dfodd2  44154  dfeven5  44184  dfodd7  44185  fpprel  44246  1hegrlfgr  44360  ismgmhm  44403  issubmgm  44409  rabsubmgmd  44411  mgmhmeql  44423  assintop  44469  isassintop  44470  assintopcllaw  44472  isrnghm  44516  isrngisom  44520  0even  44555  2even  44557  2zrngamgm  44563  dmatALTbasel  44811  lcoval  44821  elbigo  44965  elrrx2linest2  45159  itsclc0  45185  itsclc0b  45186  itscnhlinecirc02p  45199  secval  45273  cscval  45274  cotval  45275