Theorem elrab 3659

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {crab 3423  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465

This theorem is referenced by:  elrab3  3660  elrabd  3661  elrabrd  3662  elrab2  3663  ralrab  3666  rexrab  3668  reurab  3673  rabsnt  4702  unimax  4914  ssintub  4935  intminss  4943  rabxfrd  5389  ssimaex  6967  weniso  7353  canth  7365  riotarab  7410  sorpsscmpl  7732  onnminsb  7797  dfom2  7863  ssnlim  7881  elsuppfng  8164  elsuppfn  8165  ressuppssdif  8180  oeeulem  8586  cofonr  8659  elpmg  8839  fineqvlem  9225  mapfienlem2  9365  supub  9418  suplub  9419  ordtypelem6  9484  ordtypelem7  9485  hartogslem1  9503  hartogs  9505  wemapsolem  9511  card2on  9515  elharval  9522  wdom2d  9541  cantnfs  9634  scottex  9858  scottelrankd  9872  tskwe  9935  cardid2  9938  iscard2  9961  cardmin2  9984  acni3  10030  alephsuc2  10063  kmlem1  10133  cofsmo  10252  coftr  10256  fin23lem11  10300  enfin2i  10304  fin1a2lem9  10391  fin1a2lem11  10393  axcc4  10422  axdc3lem2  10434  zorn2lem7  10485  ondomon  10546  alephval2  10556  grutsk  10806  negf1o  11643  infm3  12173  nnind  12250  peano2uz2  12683  peano5uzi  12684  dfuzi  12686  uzind  12687  uzind3  12689  eluz1  12865  uzind4  12929  nnwos  12938  eqreznegel  12957  zmin  12967  elixx1  13380  elioo2  13412  elfz1  13539  flval3  13847  serge0  14091  expge0  14133  expge1  14134  hashbclem  14488  pr2pwpr  14515  elss2prb  14524  hash2sspr  14525  wrdmap  14582  wwlktovfo  14994  shftf  15115  rlimrege0  15629  incexc2  15891  dvdsdivcl  16373  divalglem4  16453  divalgmod  16463  bitsval  16481  bezout  16600  dfgcd2  16603  lcmledvds  16656  lcmgcdlem  16663  lcmfledvds  16689  1nprm  16736  1idssfct  16737  isprm2  16739  hashdvds  16833  phisum  16849  odzval  16850  odzcllem  16851  odzdvds  16854  prmreclem2  16976  prmreclem5  16979  rami  17074  ramub1lem1  17085  ramub1lem2  17086  prmgaplem3  17112  prmgaplem4  17113  prmgaplem5  17114  prmgaplem6  17115  ismre  17641  ismri  17686  isacs  17706  isacs1i  17712  catlid  17738  catrid  17739  ismon  17789  isnat  18006  eldmcoa  18121  fncnvimaeqv  18175  lubeldm  18406  glbeldm  18419  gsumval2  18743  ismgmhm  18753  issubmgm  18759  rabsubmgmd  18761  mgmhmeql  18773  ismhm  18842  issubm  18860  issubmd  18863  mndind  18886  grplinv  19055  issubg  19191  isnsg  19220  cycsubg  19278  isgim  19331  isga  19360  elcntz  19391  elcntzsn  19394  symgfix2  19485  symgsssg  19536  symgfisg  19537  psgnunilem5  19563  odid  19607  odlem2  19608  gexid  19650  gexlem2  19651  gexdvds  19653  isslw  19677  pgpssslw  19683  pj1id  19768  oddvdssubg  19924  pgpfac1lem5  20150  ablfaclem2  20157  isirred  20500  isrnghm  20522  isrngim  20526  isrim0  20563  issubrng  20631  issubrg  20655  rgspnmin  20699  issdrg  20868  isabv  20891  islss  21032  islmhm  21125  islmim  21160  islbs  21174  isprmidl  21433  psgndiflemB  21718  elocv  21786  isobs  21838  dsmmelbas  21857  frlmelbas  21874  islinds  21927  gsumbagdiaglem  22049  rhmpsrlem2  22059  psrlidm  22079  psrridm  22080  psrass1  22081  psrcom  22085  mplsubglem  22116  mpllsslem  22117  evlsval2  22206  ismhp  22271  ismhp3  22273  mhpmulcl  22280  psdmul  22297  coe1ae0  22344  coe1mul2  22398  dmatel  22618  scmatel  22630  scmateALT  22637  symgmatr01lem  22778  pmatcoe1fsupp  22826  cpmatel  22836  chpscmat  22967  istopon  23037  fctop  23129  cctop  23131  ppttop  23132  pptbas  23133  epttop  23134  iscld  23152  clscld  23172  isnei  23228  neips  23238  neiptopnei  23257  iscn  23360  iscnp  23362  cmpsublem  23524  conncompconn  23557  2ndc1stc  23576  2ndcdisj  23581  elkgen  23661  xkoccn  23744  txdis1cn  23760  txkgen  23777  xkococnlem  23784  xkococn  23785  xkoinjcn  23812  txconn  23814  elqtop  23822  elmptrab  23952  fbssfi  23962  opnfbas  23967  elfg  23996  cfinfil  24018  csdfil  24019  supfil  24020  filssufilg  24036  uffix  24046  fixufil  24047  uffixfr  24048  elflim2  24089  fclscf  24150  flimfnfcls  24153  alexsubALTlem2  24173  alexsubALTlem4  24175  alexsubALT  24176  ptcmplem2  24178  elutop  24358  isucn  24402  iscfilu  24412  ispsmet  24429  ismet  24448  isxmet  24449  elblps  24512  elbl  24513  restmetu  24695  icccmp  24951  elcncf  25016  ishtpy  25099  isphtpy  25108  om1elbas  25159  iscfil  25392  iscau  25403  iscmet  25411  lmle  25428  rrxfsupp  25529  minveclem3  25556  minveclem4  25559  ovolshftlem1  25636  ovolscalem1  25640  ovolicc2lem3  25646  dyadmax  25725  dyadmbllem  25726  opnmbllem  25728  vitalilem2  25736  vitalilem3  25737  elcpn  26061  ig1pval3  26303  coelem  26351  quotlem  26429  elqaalem1  26448  elqaalem3  26450  aannenlem1  26457  aannenlem2  26458  dmarea  27087  jensen  27118  ftalem4  27205  efnnfsumcl  27232  efchtdvds  27288  sqff1o  27311  fsumdvdsdiaglem  27312  dvdsppwf1o  27315  dvdsflf1o  27316  dvdsflsumcom  27317  musum  27320  muinv  27322  logfac2  27346  dchrelbas  27365  lgsfle1  27435  lgsle1  27441  lgsdirprm  27460  lgsne0  27464  lgsquadlem1  27509  lgsquadlem2  27510  dchrvmasumlem1  27624  logsqvma  27671  pntleml  27740  ltsval2  27785  ltsres  27791  conway  27937  cutcuts  27939  cutbday  27942  cutsun12  27948  cutbdaybnd2  27954  cutbdaylt  27956  bday1  27972  cutlt  28090  precsexlem8  28372  precsexlem9  28373  precsexlem11  28375  oncutlt  28422  noseqinds  28451  peano5uzs  28562  uzsind  28563  tgellng  28787  mircgr  28895  mirbtwn  28896  elplng  29019  iseqlg  29138  ttgelitv  29172  upgrle  29380  upgrbi  29383  umgredg2  29390  umgrbi  29391  edgupgr  29424  edgumgr  29425  upgredg  29427  numedglnl  29434  edgusgr  29450  usgruspgrb  29473  usgredg2ALT  29483  ushgredgedg  29519  ushgredgedgloop  29521  usgrexmplef  29549  upgrreslem  29594  umgrreslem  29595  upgrres1  29603  nbgrel  29630  nbupgrel  29635  nbumgrvtx  29636  nbusgreledg  29643  nbgrnself  29649  uvtxusgrel  29693  vtxdgoddnumeven  29843  rgrusgrprc  29879  lfgrwlkprop  29975  iswwlks  30125  iswwlksn  30127  wwlksnextsurj  30189  rusgrnumwwlkslem  30261  rusgrnumwwlks  30266  isclwwlk  30275  clwwlknscsh  30353  eleclclwwlkn  30367  clwlknf1oclwwlkn  30375  clwwlkvbij  30404  eupth2lems  30529  konigsberglem4  30546  fusgreg2wsplem  30624  2clwwlkel  30640  extwwlkfabel  30644  clwwlknonclwlknonf1o  30653  dlwwlknondlwlknonf1o  30656  numclwwlk2lem1  30667  numclwlk2lem2f  30668  numclwlk2lem2f1o  30670  grpoidinv2  30807  grpoinv  30817  isssp  31016  islno  31045  isblo  31074  ishmo  31103  ubthlem1  31162  ubthlem2  31163  htthlem  31209  ocel  31573  shsval2i  31679  ococin  31700  chsupsn  31705  eleigvec  32249  cnlnadjlem5  32363  shatomistici  32653  hatomistici  32654  dmrab  32783  nnindf  33104  indf1ofs  33126  ismnt  33243  pwrssmgc  33260  tocycf  33377  tocyc01  33378  trsp2cyc  33383  cycpmco2f1  33384  cycpmco2rn  33385  cycpmco2lem2  33387  cycpmco2lem3  33388  cycpmco2lem5  33390  cycpmco2lem6  33391  cycpmco2lem7  33392  cycpmconjv  33402  tocyccntz  33404  cyc3evpm  33410  cycpmgcl  33413  cyc3conja  33417  isfxp  33428  fxpgaeq  33429  elrgspnsubrun  33509  rlocisunit  33536  fldgensdrg  33577  nsgmgclem  33663  nsgmgc  33664  nsgqusf1olem2  33666  ismxidl  33689  ssmxidl  33701  isrprm  33751  1arithufdlem3  33780  1arithufdlem4  33781  1arithufd  33782  mplvrpmlem  33877  mplvrpmga  33879  mplvrpmmhm  33880  fedgmullem2  33964  ply1annnr  34037  minplyann  34043  minplyirred  34045  constrsuc  34072  zarclsiin  34205  zart0  34213  rhmpreimacnlem  34218  ordtconnlem1  34258  sigagenval  34474  ldsysgenld  34494  ldgenpisyslem1  34497  ldgenpisyslem2  34498  ldgenpisys  34500  ddemeas  34570  ismbfm  34585  imambfm  34596  dya2iocuni  34617  oms0  34631  omssubadd  34634  elcarsg  34639  issibf  34667  sitgfval  34675  oddpwdc  34688  eulerpartlemgh  34712  eulerpartlemgs2  34714  dstfrvel  34808  ballotlemfc0  34827  ballotlemfcc  34828  ballotlemiex  34836  ballotlemfrcn0  34864  ballotlemirc  34866  ballotlem7  34870  reprsum  34944  reprsuc  34946  reprpmtf1o  34957  reprdifc  34958  fnrelpredd  35424  fineqvnttrclselem2  35457  connpconn  35625  iscvm  35649  cvmsi  35655  cvmsval  35656  cvmliftmolem2  35672  cvmliftiota  35691  snmlval  35721  satfv1lem  35752  fmlafvel  35775  fmla1  35777  fmlaomn0  35780  satfv0fvfmla0  35803  sategoelfvb  35809  elmpst  35926  lineelsb2  36538  linerflx1  36539  fwddifval  36552  fwddifnval  36553  rankeq1o  36561  finminlem  36717  fneint  36747  fnessref  36756  topmeet  36763  topjoin  36764  neifg  36770  weiunlem  36862  weiunfrlem  36863  weiunse  36867  regsfromregtco  36937  relowlssretop  37896  fin2solem  38144  fin2so  38145  poimirlem4  38162  poimirlem25  38183  poimirlem26  38184  poimirlem27  38185  poimirlem31  38189  poimirlem32  38190  opnmbllem0  38194  mblfinlem2  38196  itg2gt0cn  38213  indexa  38271  nninfnub  38289  istotbnd  38307  sstotbnd2  38312  isbnd  38318  isrngohom  38503  isrngoiso  38516  isidl  38552  ispridl  38572  ismaxidl  38578  prnc  38605  isfldidl  38606  islshp  39642  lssats  39675  islfl  39723  isat  39949  atlatmstc  39982  islln  40169  islpln  40193  islvol  40236  linepsubN  40415  elpmap  40421  pmapsub  40431  elpadd  40462  paddvaln0N  40464  islhp  40659  isldil  40773  isltrn  40782  isdilN  40817  istrnN  40820  diaval  41695  diaelval  41696  diaeldm  41699  diaelrnN  41708  cdlemm10N  41781  docaclN  41787  dibglbN  41829  dicval  41839  dicfnN  41846  dicvalrelN  41848  dihglblem2aN  41956  dihglblem2N  41957  dihglblem3N  41958  dih1dimatlem  41992  dihglb2  42005  dochvalr  42020  doch2val2  42027  dochocss  42029  islpolN  42146  mapd0  42328  aks4d1p4  42735  aks4d1p7  42739  isprimroot  42749  linvh  42752  primrootsunit1  42753  primrootscoprmpow  42755  primrootscoprbij  42758  sticksstones3  42804  aks6d1c6lem3  42828  grpods  42850  unitscyglem2  42852  unitscyglem4  42854  unitscyglem5  42855  supinf  42899  fsuppssindlem2  43215  infdesc  43266  isnacs  43326  elmzpcl  43348  mzpindd  43368  rencldnfilem  43438  irrapxlem6  43445  pellexlem3  43449  pellexlem5  43451  elpell1qr  43465  elpell14qr  43467  elpell1234qr  43469  pellfundre  43499  pellfundge  43500  pellfundlb  43502  pellfundglb  43503  rmspecnonsq  43525  jm2.22  43613  jm2.23  43614  rpnnen3lem  43649  fnwe2lem2  43669  elmnc  43754  dgraalem  43763  dgraaub  43766  mpaalem  43770  onsucelab  43881  limnsuc  43883  sqrtcvallem1  44248  rfovcnvf1od  44621  nzss  44918  iccshift  46125  iooshift  46129  limcperiod  46235  sumnnodd  46237  ioodvbdlimc1lem1  46536  dvnprodlem1  46551  dvnprodlem3  46553  itgperiod  46586  stoweidlem14  46619  stoweidlem15  46620  stoweidlem16  46621  stoweidlem31  46636  stoweidlem36  46641  stoweidlem46  46651  stoweidlem48  46653  fourierdlem2  46714  fourierdlem3  46715  fourierdlem20  46732  fourierdlem25  46737  fourierdlem37  46749  fourierdlem42  46754  fourierdlem48  46759  fourierdlem51  46762  fourierdlem63  46774  fourierdlem64  46775  fourierdlem65  46776  fourierdlem79  46790  fourierdlem81  46792  elaa2lem  46838  etransclem24  46863  etransclem26  46865  etransclem28  46867  etransclem35  46874  etransclem48  46887  salgenval  46926  salgenn0  46936  salgencl  46937  sssalgen  46940  salgenss  46941  salgenuni  46942  issalgend  46943  salgencntex  46948  subsaliuncllem  46962  sge0fodjrnlem  47021  meadjiunlem  47070  caragenel  47100  ovnlecvr  47163  ovnpnfelsup  47164  ovncvrrp  47169  ovnsubaddlem1  47175  hoidmv1lelem1  47196  hoidmv1lelem2  47197  hoidmv1lelem3  47198  hoidmvlelem1  47200  hoidmvlelem2  47201  hoidmvlelem4  47203  ovnhoilem1  47206  ovnlecvr2  47215  ovncvr2  47216  issmflem  47332  smflimlem2  47377  smflimlem3  47378  smflimsuplem2  47426  elsetpreimafvrab  48031  iccpart  48053  sprel  48121  prelspr  48123  sprsymrelfolem2  48130  sprsymrelf  48132  prpair  48138  paireqne  48148  prprelb  48153  prprelprb  48154  dfodd2  48289  dfeven5  48319  dfodd7  48320  fpprel  48381  clnbgrel  48481  clnbupgrel  48487  sclnbgrel  48500  vopnbgrel  48507  dfclnbgr6  48509  dfnbgr6  48510  isubgredg  48519  uhgrimisgrgric  48584  grtriprop  48594  isgrtri  48596  stgredgel  48610  stgrusgra  48612  uspgrlimlem3  48643  uspgrlim  48645  grlimgredgex  48653  grlimgrtrilem2  48655  gpgiedgdmel  48702  gpgedgel  48703  gpgnbgrvtx0  48727  gpgnbgrvtx1  48728  gpgprismgr4cycllem10  48757  1hegrlfgr  48785  assintop  48862  isassintop  48863  assintopcllaw  48865  0even  48890  2even  48892  2zrngamgm  48898  dmatALTbasel  49066  lcoval  49076  elbigo  49215  elrrx2linest2  49409  itsclc0  49435  itsclc0b  49436  itscnhlinecirc02p  49449  unilbss  49480  secval  50409  cscval  50410  cotval  50411