Theorem elrabd 3647

Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3645. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
elrabd.1	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
elrabd.2	⊢ (𝜑 → 𝐴 ∈ 𝐵)
elrabd.3	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
elrabd	⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜒,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem elrabd

Step	Hyp	Ref	Expression
1		elrabd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		elrabd.3	. 2 ⊢ (𝜑 → 𝜒)
3		elrabd.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜒))
4	3	elrab 3645	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓} ↔ (𝐴 ∈ 𝐵 ∧ 𝜒))
5	1, 2, 4	sylanbrc 595	1 ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452

This theorem is used by:  nnawordex  8625  cofon1  8660  ordtypelem7  9496  oemapvali  9663  rankuni2b  9835  harval2  10002  fin23lem11  10319  fin1a2lem11  10412  pinq  10936  negf1o  11668  uzind4  12955  zsupss  12986  flval3  13876  serge0  14120  expge0  14162  expge1  14163  hashbclem  14517  rlimrege0  15666  lcmgcdlem  16696  phicl2  16859  hashdvds  16866  phisum  16882  pcpremul  16935  prmreclem1  17008  prmreclem3  17010  prmreclem5  17012  ramub  17105  ramub1lem1  17118  ramub1lem2  17119  prmgaplem3  17145  prmgaplem4  17146  prmgaplem5  17147  prmgaplem6  17148  mrcflem  17694  mrcval  17698  isacs1i  17745  coaval  18157  gsumress  18784  rabsubmgmd  18806  issubmd  18914  mhmeql  18935  ghmeql  19366  pmtrval  19578  pmtrrn  19584  symgsssg  19594  symgfisg  19595  psgnunilem5  19621  pgpssslw  19741  efgsfo  19866  oddvdssubg  19982  dprdwd  20140  lmhmeql  21239  ssdifidllem  21547  ssdifidl  21548  cofipsgn  21806  frlmssuvc2  22008  gsumbagdiaglem  22146  psrlidm  22176  psrridm  22177  mplmonmul  22252  mhpmulcl  22377  psdmul  22394  coe1fsupp  22439  dmatmulcl  22722  fctop  23229  cctop  23231  ppttop  23232  pptbas  23233  epttop  23234  ordthauslem  23608  cmpsublem  23624  locfincmp  23752  xkoopn  23815  pthaus  23864  txkgen  23878  xkohaus  23879  xkococnlem  23885  nrmr0reg  23975  fbssfi  24063  filssufilg  24137  uffixsn  24151  ufinffr  24155  ufilen  24156  supnfcls  24246  flimfnfcls  24254  alexsubALTlem4  24276  tmdgsum2  24322  symgtgp  24332  ghmcnp  24341  lmle  25529  iundisj  25776  opnmbllem  25829  vitalilem2  25837  aannenlem2  26565  aalioulem2  26569  radcnv0  26652  jensen  27225  ftalem4  27312  ftalem5  27313  efnnfsumcl  27339  efchtdvds  27395  sqff1o  27418  fsumdvdsdiaglem  27419  dvdsppwf1o  27422  dvdsflf1o  27423  muinv  27429  dchrfi  27491  lgsne0  27571  2lgslem1b  27628  cutbdaybnd  28060  madebdaylemlrcut  28164  sltsbday  28182  cofcut1  28185  cofcutr  28189  noseqinds  28558  onsfi  28621  elcgrabasrd  29255  cgrabasimass  29257  upgr1elem  29569  subumgredg2  29745  subupgr  29747  upgrreslem  29764  umgrreslem  29765  1hevtxdg1  29966  umgr2v2e  29985  pwrssmgc  33440  tocycfv  33549  cycpm3cl2  33576  elrgspnlem1  33682  elrgspnlem2  33683  elrgspnlem3  33684  elrgspnlem4  33685  elrgspnsubrunlem1  33687  fldgensdrg  33755  fldgenssv  33756  fldgenssp  33759  nsgmgclem  33840  nsgmgc  33841  nsgqusf1olem2  33843  ssmxidllem  33876  ssmxidl  33877  1arithufdlem1  33954  1arithufdlem2  33955  1arithufdlem3  33956  1arithufdlem4  33957  0mplrim  34024  selvply1rhmlema  34028  selvply1rhmlemb  34029  selvply1rhmlem1  34030  selvply1rhmlem2  34031  selvply1rhmlem4  34033  selvply1rhm0  34036  extvfvvcl  34045  extvfvcl  34046  mplmulmvr  34049  evlextv  34052  mplvrpmlem  34053  mplvrpmfgalem  34054  mplvrpmga  34055  mplvrpmmhm  34056  mplvrpmrhm  34057  psrmonmul  34060  psrmonprod  34062  esplyfval0  34074  esplylem  34076  esplyfv1  34079  esplyfvaln  34084  esplyind  34085  minplymindeg  34218  minplyirredlem  34220  irngnminplynz  34222  irredminply  34226  zarcls1  34379  zarclsiin  34381  zart0  34389  ldgenpisyslem1  34674  fmla1  35966  aks4d1p5  42946  aks4d1p8  42953  primrootsunit1  42963  primrootscoprmpow  42965  primrootscoprbij  42968  hashscontpow1  42987  sticksstones2  43013  grpods  43060  unitscyglem1  43061  unitscyglem2  43062  unitscyglem4  43064  supinf  43109  fnwe2lem2  43892  fnwe2lem3  43893  onintunirab  44068  naddwordnexlem4  44242  supminfrnmpt  46273  supminfxr  46292  supminfxr2  46297  supminfxrrnmpt  46299  dvnprodlem1  46774  smflimsuplem5  47652  tmachlem-agreeself  47764  lubprlem  49888  intubeu  49910  unilbeu  49911