Theorem elrabd 3651

Description: Membership in a restricted class abstraction, using implicit substitution. Deduction version of elrab 3649. (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 3649	. 2 ⊢ (𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓} ↔ (𝐴 ∈ 𝐵 ∧ 𝜒))
5	1, 2, 4	sylanbrc 594	1 ⊢ (𝜑 → 𝐴 ∈ {𝑥 ∈ 𝐵 ∣ 𝜓})

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   ∈ wcel 2142  {crab 3415

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456

This theorem is used by:  nnawordex  8621  cofon1  8656  ordtypelem7  9484  oemapvali  9651  rankuni2b  9823  harval2  9990  fin23lem11  10307  fin1a2lem11  10400  pinq  10918  negf1o  11650  uzind4  12936  zsupss  12967  flval3  13855  serge0  14099  expge0  14141  expge1  14142  hashbclem  14496  rlimrege0  15637  lcmgcdlem  16670  phicl2  16833  hashdvds  16840  phisum  16856  pcpremul  16909  prmreclem1  16982  prmreclem3  16984  prmreclem5  16986  ramub  17079  ramub1lem1  17092  ramub1lem2  17093  prmgaplem3  17119  prmgaplem4  17120  prmgaplem5  17121  prmgaplem6  17122  mrcflem  17668  mrcval  17672  isacs1i  17719  coaval  18131  gsumress  18746  rabsubmgmd  18768  issubmd  18870  mhmeql  18891  ghmeql  19315  pmtrval  19527  pmtrrn  19533  symgsssg  19543  symgfisg  19544  psgnunilem5  19570  pgpssslw  19690  efgsfo  19815  oddvdssubg  19931  dprdwd  20089  lmhmeql  21187  ssdifidllem  21495  ssdifidl  21496  cofipsgn  21754  frlmssuvc2  21956  gsumbagdiaglem  22092  psrlidm  22122  psrridm  22123  mplmonmul  22198  mhpmulcl  22323  psdmul  22340  coe1fsupp  22385  dmatmulcl  22668  fctop  23172  cctop  23174  ppttop  23175  pptbas  23176  epttop  23177  ordthauslem  23551  cmpsublem  23567  locfincmp  23694  xkoopn  23757  pthaus  23806  txkgen  23820  xkohaus  23821  xkococnlem  23827  nrmr0reg  23917  fbssfi  24005  filssufilg  24079  uffixsn  24093  ufinffr  24097  ufilen  24098  supnfcls  24188  flimfnfcls  24196  alexsubALTlem4  24218  tmdgsum2  24264  symgtgp  24274  ghmcnp  24283  lmle  25471  iundisj  25718  opnmbllem  25771  vitalilem2  25779  aannenlem2  26503  aalioulem2  26507  radcnv0  26590  jensen  27164  ftalem4  27251  ftalem5  27252  efnnfsumcl  27278  efchtdvds  27334  sqff1o  27357  fsumdvdsdiaglem  27358  dvdsppwf1o  27361  dvdsflf1o  27362  muinv  27368  dchrfi  27430  lgsne0  27510  2lgslem1b  27567  cutbdaybnd  27999  madebdaylemlrcut  28103  sltsbday  28121  cofcut1  28124  cofcutr  28128  noseqinds  28497  onsfi  28560  upgr1elem  29473  subumgredg2  29646  subupgr  29648  upgrreslem  29665  umgrreslem  29666  1hevtxdg1  29867  umgr2v2e  29886  pwrssmgc  33329  tocycfv  33438  cycpm3cl2  33465  elrgspnlem1  33571  elrgspnlem2  33572  elrgspnlem3  33573  elrgspnlem4  33574  elrgspnsubrunlem1  33576  fldgensdrg  33644  fldgenssv  33645  fldgenssp  33648  nsgmgclem  33729  nsgmgc  33730  nsgqusf1olem2  33732  ssmxidllem  33765  ssmxidl  33766  1arithufdlem1  33843  1arithufdlem2  33844  1arithufdlem3  33845  1arithufdlem4  33846  0mplrim  33913  selvply1rhmlema  33917  selvply1rhmlemb  33918  selvply1rhmlem1  33919  selvply1rhmlem2  33920  selvply1rhmlem4  33922  selvply1rhm0  33925  extvfvvcl  33934  extvfvcl  33935  mplmulmvr  33938  evlextv  33941  mplvrpmlem  33942  mplvrpmfgalem  33943  mplvrpmga  33944  mplvrpmmhm  33945  mplvrpmrhm  33946  psrmonmul  33949  psrmonprod  33951  esplyfval0  33963  esplylem  33965  esplyfv1  33968  esplyfvaln  33973  esplyind  33974  minplymindeg  34107  minplyirredlem  34109  irngnminplynz  34111  irredminply  34115  zarcls1  34268  zarclsiin  34270  zart0  34278  ldgenpisyslem1  34562  fmla1  35887  aks4d1p5  42875  aks4d1p8  42882  primrootsunit1  42892  primrootscoprmpow  42894  primrootscoprbij  42897  hashscontpow1  42916  sticksstones2  42942  grpods  42989  unitscyglem1  42990  unitscyglem2  42991  unitscyglem4  42993  supinf  43038  fnwe2lem2  43806  fnwe2lem3  43807  onintunirab  43982  naddwordnexlem4  44156  supminfrnmpt  46187  supminfxr  46206  supminfxr2  46211  supminfxrrnmpt  46213  dvnprodlem1  46688  smflimsuplem5  47566  lubprlem  49768  intubeu  49790  unilbeu  49791