Theorem elrabd 3685

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536   ∈ wcel 2113  {crab 3145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499

This theorem is referenced by:  nnawordex  8266  ordtypelem7  8991  oemapvali  9150  rankuni2b  9285  harval2  9429  fin23lem11  9742  fin1a2lem11  9835  pinq  10352  negf1o  11073  fiminreOLD  11593  uzind4  12309  zsupss  12340  flval3  13188  serge0  13427  expge0  13468  expge1  13469  hashbclem  13813  rlimrege0  14939  lcmgcdlem  15953  phicl2  16108  hashdvds  16115  phisum  16130  pcpremul  16183  prmreclem1  16255  prmreclem3  16257  prmreclem5  16259  ramub  16352  ramub1lem1  16365  ramub1lem2  16366  prmgaplem3  16392  prmgaplem4  16393  prmgaplem5  16394  prmgaplem6  16395  mrcflem  16880  mrcval  16884  isacs1i  16931  coaval  17331  gsumress  17895  issubmd  17974  mhmeql  17993  ghmeql  18384  pmtrval  18582  pmtrrn  18588  symgsssg  18598  symgfisg  18599  psgnunilem5  18625  pgpssslw  18742  efgsfo  18868  oddvdssubg  18978  dprdwd  19136  lmhmeql  19830  gsumbagdiaglem  20158  psrlidm  20186  psrridm  20187  mplmonmul  20248  coe1fsupp  20385  cofipsgn  20740  frlmssuvc2  20942  dmatmulcl  21112  fctop  21615  cctop  21617  ppttop  21618  pptbas  21619  epttop  21620  ordthauslem  21994  cmpsublem  22010  locfincmp  22137  xkoopn  22200  pthaus  22249  txkgen  22263  xkohaus  22264  xkococnlem  22270  nrmr0reg  22360  fbssfi  22448  filssufilg  22522  uffixsn  22536  ufinffr  22540  ufilen  22541  supnfcls  22631  flimfnfcls  22639  alexsubALTlem4  22661  tmdgsum2  22707  symgtgp  22717  ghmcnp  22726  lmle  23907  iundisj  24152  opnmbllem  24205  vitalilem2  24213  aannenlem2  24921  aalioulem2  24925  radcnv0  25007  jensen  25569  ftalem4  25656  ftalem5  25657  efnnfsumcl  25683  efchtdvds  25739  sqff1o  25762  fsumdvdsdiaglem  25763  dvdsppwf1o  25766  dvdsflf1o  25767  muinv  25773  dchrfi  25834  lgsne0  25914  2lgslem1b  25971  upgr1elem  26900  subumgredg2  27070  subupgr  27072  upgrreslem  27089  umgrreslem  27090  1hevtxdg1  27291  umgr2v2e  27310  tocycfv  30755  cycpm3cl2  30782  ssmxidllem  30982  ssmxidl  30983  ldgenpisyslem1  31426  fmla1  32638  fnwe2lem2  39657  fnwe2lem3  39658  supminfrnmpt  41725  supminfxr  41746  supminfxr2  41751  supminfxrrnmpt  41753  smflimsuplem5  43105  rabsubmgmd  44065