Theorem r19.21aiv 1259

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)

Hypothesis

Ref	Expression
r19.21aiv.1	⊢ (φ → (x ∈ A → ψ))

Assertion

Ref	Expression
r19.21aiv	⊢ (φ → ∀x ∈ A ψ)

Distinct variable group(s):   φ,x

Proof of Theorem r19.21aiv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 ⊢ (φ → ∀xφ)
2		r19.21aiv.1	. 2 ⊢ (φ → (x ∈ A → ψ))
3	1, 2	r19.21ai 1258	1 ⊢ (φ → ∀x ∈ A ψ)

Syntax hints:   → wi 2   ∈ wcel 1092  ∀wral 1201

This theorem is referenced by:  r19.21aivv 1263  rgen2a 1264  rgen3 1265  nrexdv 1271  r19.37av 1300  rzal 1773  iuneq2dv 2010  iineq2dv 2011  trin 2051  supsn 2168  ssorduni 2249  ordunidif 2260  onmindif 2312  onmindif2 2313  suceloni 2314  ralxp 2456  dmxp 2552  dffun7 2688  cleqfv 2880  ffnfv 2892  fconst2 2902  fconstfv 2903  abrexex 2912  isocnv 2934  isotr 2935  isowe 2941  f1oiso 2942  tfrlem10 2958  tfrlem12 2960  tz7.48-2 2995  oaass 3163  omsmo 3196  en2d 3303  dom2d 3307  pw2en 3348  mapenlem2 3385  xpmapenlem4 3394  xpmapenlem5 3395  unblem4 3434  unbnn2 3436  fiint 3445  eirrv 3449  trcl 3489  r1tr 3498  r1val1 3502  tz9.13 3507  r1val3 3523  rankr1id 3539  scottex 3541  scott0 3542  aceq3 3556  aceq5lem5 3562  ac6lem 3575  kmlem4 3583  kmlem10 3589  numthlem 3598  ondomon 3662  ondomcard 3663  cardmin 3666  carduniima 3695  cfsuc 3709  genpcl 3905  ltexprlem5 3940  suplem1pr 3955  negeu 4124  receu 4215  uzwo 4605  nnwoOLD 4608  uzwo3lem1 4614  uzwo3lem2 4615  seqrn 4673  clim0 4882  infxpidmlem7 4939  hial2eqt 5060  hlim0 5140  ocsh 5164  occont 5168  occllem4 5183  occl 5188  projlem24 5216  projlem26 5218  projlem29 5221  projlem31 5223  pjthlem14 5238  pjthu 5241  pjthu2 5242  shintcl 5294  hsupss 5310  spanss 5319  spansn 5462  osumlem5 5534  pjss1co 5633  pjss2co 5634  pjnormss 5638  pjorthco 5639  pjscj 5640  pjclem4 5653  pj3s 5659  pj3cor1 5661  strlem3a 5693  strb 5699  spansncv2t 5725  ssmd1 5734  h1dat 5747  chrelat2 5758  mdsymlem6 5781  sumdmdi 5785

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-ral 1205

metamath.org