Theorem elrab 3680

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {crab 3142  Vcvv 3494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496

This theorem is referenced by:  elrab3  3681  elrabd  3682  elrab2  3683  ralrab  3685  rexrab  3687  rabsnt  4667  unimax  4874  ssintub  4894  intminss  4902  rabxfrd  5318  ssimaex  6748  weniso  7107  canth  7111  sorpsscmpl  7460  onnminsb  7519  dfom2  7582  ssnlim  7599  elsuppfn  7838  ressuppssdif  7851  oeeulem  8227  elpmg  8422  fineqvlem  8732  mapfienlem2  8869  supub  8923  suplub  8924  ordtypelem6  8987  ordtypelem7  8988  hartogslem1  9006  hartogs  9008  wemapsolem  9014  card2on  9018  elharval  9027  wdom2d  9044  cantnfs  9129  scottex  9314  tskwe  9379  cardid2  9382  iscard2  9405  cardmin2  9427  acni3  9473  alephsuc2  9506  kmlem1  9576  cofsmo  9691  coftr  9695  fin23lem11  9739  enfin2i  9743  fin1a2lem9  9830  fin1a2lem11  9832  axcc4  9861  axdc3lem2  9873  zorn2lem7  9924  ondomon  9985  alephval2  9994  grutsk  10244  negf1o  11070  fiminreOLD  11590  infm3  11600  nnind  11656  peano2uz2  12071  peano5uzi  12072  dfuzi  12074  uzind  12075  uzind3  12077  eluz1  12248  uzind4  12307  nnwos  12316  eqreznegel  12335  zmin  12345  elixx1  12748  elioo2  12780  elfz1  12898  flval3  13186  serge0  13425  expge0  13466  expge1  13467  hashbclem  13811  pr2pwpr  13838  elss2prb  13846  hash2sspr  13847  wrdmap  13897  wwlktovfo  14322  shftf  14438  rlimrege0  14936  incexc2  15193  dvdsdivcl  15666  divalglem4  15747  divalgmod  15757  bitsval  15773  bezout  15891  dfgcd2  15894  lcmledvds  15943  lcmgcdlem  15950  lcmfledvds  15976  1nprm  16023  1idssfct  16024  isprm2  16026  hashdvds  16112  phisum  16127  odzval  16128  odzcllem  16129  odzdvds  16132  prmreclem2  16253  prmreclem5  16256  rami  16351  ramub1lem1  16362  ramub1lem2  16363  prmgaplem3  16389  prmgaplem4  16390  prmgaplem5  16391  prmgaplem6  16392  ismre  16861  ismri  16902  isacs  16922  isacs1i  16928  catlid  16954  catrid  16955  ismon  17003  isnat  17217  eldmcoa  17325  fncnvimaeqv  17370  lubeldm  17591  glbeldm  17604  gsumval2  17896  ismhm  17958  issubm  17968  issubmd  17971  mndind  17992  grplinv  18152  issubg  18279  isnsg  18307  cycsubg  18351  isgim  18402  isga  18421  elcntz  18452  elcntzsn  18455  symgfix2  18544  symgsssg  18595  symgfisg  18596  psgnunilem5  18622  odid  18666  odlem2  18667  gexid  18706  gexlem2  18707  gexdvds  18709  isslw  18733  pgpssslw  18739  pj1id  18825  oddvdssubg  18975  pgpfac1lem5  19201  ablfaclem2  19208  isirred  19449  isrim0  19475  issubrg  19535  issdrg  19574  isabv  19590  islss  19706  islmhm  19799  islmim  19834  islbs  19848  gsumbagdiaglem  20155  psrmulcllem  20167  psrlidm  20183  psrridm  20184  psrass1  20185  psrcom  20189  mplsubglem  20214  mpllsslem  20215  evlsval2  20300  ismhp  20334  coe1ae0  20384  coe1mul2  20437  psgndiflemB  20744  elocv  20812  isobs  20864  dsmmelbas  20883  frlmelbas  20900  islinds  20953  dmatel  21102  scmatel  21114  scmateALT  21121  symgmatr01lem  21262  pmatcoe1fsupp  21309  cpmatel  21319  chpscmat  21450  istopon  21520  fctop  21612  cctop  21614  ppttop  21615  pptbas  21616  epttop  21617  iscld  21635  clscld  21655  isnei  21711  neips  21721  neiptopnei  21740  iscn  21843  iscnp  21845  cmpsublem  22007  conncompconn  22040  2ndc1stc  22059  2ndcdisj  22064  elkgen  22144  xkoccn  22227  txdis1cn  22243  txkgen  22260  xkococnlem  22267  xkococn  22268  xkoinjcn  22295  txconn  22297  elqtop  22305  elmptrab  22435  fbssfi  22445  opnfbas  22450  elfg  22479  cfinfil  22501  csdfil  22502  supfil  22503  filssufilg  22519  uffix  22529  fixufil  22530  uffixfr  22531  elflim2  22572  fclscf  22633  flimfnfcls  22636  alexsubALTlem2  22656  alexsubALTlem4  22658  alexsubALT  22659  ptcmplem2  22661  elutop  22842  isucn  22887  iscfilu  22897  ispsmet  22914  ismet  22933  isxmet  22934  elblps  22997  elbl  22998  restmetu  23180  icccmp  23433  elcncf  23497  ishtpy  23576  isphtpy  23585  om1elbas  23636  iscfil  23868  iscau  23879  iscmet  23887  lmle  23904  rrxfsupp  24005  minveclem3  24032  minveclem4  24035  ovolshftlem1  24110  ovolscalem1  24114  ovolicc2lem3  24120  dyadmax  24199  dyadmbllem  24200  opnmbllem  24202  vitalilem2  24210  vitalilem3  24211  elcpn  24531  ig1pval3  24768  coelem  24816  quotlem  24889  elqaalem1  24908  elqaalem3  24910  aannenlem1  24917  aannenlem2  24918  dmarea  25535  jensen  25566  ftalem4  25653  efnnfsumcl  25680  efchtdvds  25736  sqff1o  25759  fsumdvdsdiaglem  25760  dvdsppwf1o  25763  dvdsflf1o  25764  dvdsflsumcom  25765  musum  25768  muinv  25770  logfac2  25793  dchrelbas  25812  lgsfle1  25882  lgsle1  25888  lgsdirprm  25907  lgsne0  25911  lgsquadlem1  25956  lgsquadlem2  25957  dchrvmasumlem1  26071  logsqvma  26118  pntleml  26187  tgellng  26339  mircgr  26443  mirbtwn  26444  iseqlg  26653  ttgelitv  26669  upgrle  26875  upgrbi  26878  umgredg2  26885  umgrbi  26886  edgupgr  26919  edgumgr  26920  upgredg  26922  numedglnl  26929  edgusgr  26945  usgruspgrb  26966  usgredg2ALT  26975  ushgredgedg  27011  ushgredgedgloop  27013  usgrexmplef  27041  upgrreslem  27086  umgrreslem  27087  upgrres1  27095  nbgrel  27122  nbupgrel  27127  nbumgrvtx  27128  nbusgreledg  27135  nbgrnself  27141  uvtxusgrel  27185  vtxdgoddnumeven  27335  rgrusgrprc  27371  lfgrwlkprop  27469  iswwlks  27614  iswwlksn  27616  wwlksnextsurj  27678  rusgrnumwwlkslem  27748  rusgrnumwwlks  27753  isclwwlk  27762  clwwlknscsh  27841  eleclclwwlkn  27855  clwlknf1oclwwlkn  27863  clwwlkvbij  27892  eupth2lems  28017  konigsberglem4  28034  fusgreg2wsplem  28112  2clwwlkel  28128  extwwlkfabel  28132  clwwlknonclwlknonf1o  28141  dlwwlknondlwlknonf1o  28144  numclwwlk2lem1  28155  numclwlk2lem2f  28156  numclwlk2lem2f1o  28158  grpoidinv2  28292  grpoinv  28302  isssp  28501  islno  28530  isblo  28559  ishmo  28588  ubthlem1  28647  ubthlem2  28648  htthlem  28694  ocel  29058  shsval2i  29164  ococin  29185  chsupsn  29190  eleigvec  29734  cnlnadjlem5  29848  shatomistici  30138  hatomistici  30139  dmrab  30260  nnindf  30535  tocycf  30759  tocyc01  30760  trsp2cyc  30765  cycpmco2f1  30766  cycpmco2rn  30767  cycpmco2lem2  30769  cycpmco2lem3  30770  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2lem7  30774  cycpmconjv  30784  tocyccntz  30786  cyc3evpm  30792  cycpmgcl  30795  cycpmconjslem2  30797  cyc3conja  30799  isprmidl  30955  ismxidl  30971  ssmxidl  30979  fedgmullem2  31026  ordtconnlem1  31167  indf1ofs  31285  sigagenval  31399  ldsysgenld  31419  ldgenpisyslem1  31422  ldgenpisyslem2  31423  ldgenpisys  31425  ddemeas  31495  ismbfm  31510  imambfm  31520  dya2iocuni  31541  oms0  31555  omssubadd  31558  elcarsg  31563  issibf  31591  sitgfval  31599  oddpwdc  31612  eulerpartlemgh  31636  eulerpartlemgs2  31638  dstfrvel  31731  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemiex  31759  ballotlemfrcn0  31787  ballotlemirc  31789  ballotlem7  31793  reprsum  31884  reprsuc  31886  reprpmtf1o  31897  reprdifc  31898  connpconn  32482  iscvm  32506  cvmsi  32512  cvmsval  32513  cvmliftmolem2  32529  cvmliftiota  32548  snmlval  32578  satfv1lem  32609  fmlafvel  32632  fmla1  32634  fmlaomn0  32637  satfv0fvfmla0  32660  sategoelfvb  32666  elmpst  32783  sltval2  33163  sltres  33169  conway  33264  scutcut  33266  scutbday  33267  scutun12  33271  scutbdaybnd  33275  scutbdaylt  33276  lineelsb2  33609  linerflx1  33610  fwddifval  33623  fwddifnval  33624  rankeq1o  33632  finminlem  33666  fneint  33696  fnessref  33705  topmeet  33712  topjoin  33713  neifg  33719  relowlssretop  34647  fin2solem  34893  fin2so  34894  poimirlem4  34911  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem31  34938  poimirlem32  34939  opnmbllem0  34943  mblfinlem2  34945  itg2gt0cn  34962  indexa  35023  nninfnub  35041  istotbnd  35062  sstotbnd2  35067  isbnd  35073  isrngohom  35258  isrngoiso  35271  isidl  35307  ispridl  35327  ismaxidl  35333  prnc  35360  isfldidl  35361  islshp  36130  lssats  36163  islfl  36211  isat  36437  atlatmstc  36470  islln  36657  islpln  36681  islvol  36724  linepsubN  36903  elpmap  36909  pmapsub  36919  elpadd  36950  paddvaln0N  36952  islhp  37147  isldil  37261  isltrn  37270  isdilN  37305  istrnN  37308  diaval  38183  diaelval  38184  diaeldm  38187  diaelrnN  38196  cdlemm10N  38269  docaclN  38275  dibglbN  38317  dicval  38327  dicfnN  38334  dicvalrelN  38336  dihglblem2aN  38444  dihglblem2N  38445  dihglblem3N  38446  dih1dimatlem  38480  dihglb2  38493  dochvalr  38508  doch2val2  38515  dochocss  38517  islpolN  38634  mapd0  38816  isnacs  39350  elmzpcl  39372  mzpindd  39392  rencldnfilem  39466  irrapxlem6  39473  pellexlem3  39477  pellexlem5  39479  elpell1qr  39493  elpell14qr  39495  elpell1234qr  39497  pellfundre  39527  pellfundge  39528  pellfundlb  39530  pellfundglb  39531  rmspecnonsq  39553  jm2.22  39641  jm2.23  39642  rpnnen3lem  39677  fnwe2lem2  39700  elmnc  39785  dgraalem  39794  dgraaub  39797  mpaalem  39801  rgspnmin  39820  rfovcnvf1od  40399  scottelrankd  40632  nzss  40698  iccshift  41843  iooshift  41847  limcperiod  41958  sumnnodd  41960  ioodvbdlimc1lem1  42265  dvnprodlem1  42280  dvnprodlem3  42282  itgperiod  42315  stoweidlem14  42348  stoweidlem15  42349  stoweidlem16  42350  stoweidlem31  42365  stoweidlem36  42370  stoweidlem46  42380  stoweidlem48  42382  fourierdlem2  42443  fourierdlem3  42444  fourierdlem20  42461  fourierdlem25  42466  fourierdlem37  42478  fourierdlem42  42483  fourierdlem48  42488  fourierdlem51  42491  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem79  42519  fourierdlem81  42521  elaa2lem  42567  etransclem24  42592  etransclem26  42594  etransclem28  42596  etransclem35  42603  etransclem48  42616  salgenval  42655  salgenn0  42663  salgencl  42664  sssalgen  42667  salgenss  42668  salgenuni  42669  issalgend  42670  salgencntex  42675  subsaliuncllem  42689  sge0fodjrnlem  42747  meadjiunlem  42796  caragenel  42826  ovnlecvr  42889  ovnpnfelsup  42890  ovncvrrp  42895  ovnsubaddlem1  42901  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem4  42929  ovnhoilem1  42932  ovnlecvr2  42941  ovncvr2  42942  issmflem  43053  smflimlem2  43097  smflimlem3  43098  smflimsuplem2  43144  elsetpreimafvrab  43603  iccpart  43625  sprel  43695  prelspr  43697  sprsymrelfolem2  43704  sprsymrelf  43706  prpair  43712  paireqne  43722  prprelb  43727  prprelprb  43728  dfodd2  43850  dfeven5  43880  dfodd7  43881  fpprel  43942  1hegrlfgr  44056  ismgmhm  44099  issubmgm  44105  rabsubmgmd  44107  mgmhmeql  44119  assintop  44165  isassintop  44166  assintopcllaw  44168  isrnghm  44212  isrngisom  44216  0even  44251  2even  44253  2zrngamgm  44259  dmatALTbasel  44506  lcoval  44516  elbigo  44660  elrrx2linest2  44781  itsclc0  44807  itsclc0b  44808  itscnhlinecirc02p  44821  secval  44895  cscval  44896  cotval  44897