Theorem ralrimiva 2698

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 2-Jan-2006.)

Hypothesis

Ref	Expression
ralrimiva.1	⊢ ((φ ∧ x ∈ A) → ψ)

Assertion

Ref	Expression
ralrimiva	⊢ (φ → ∀x ∈ A ψ)

Distinct variable group:   φ,x

Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem ralrimiva

Step	Hyp	Ref	Expression
1		ralrimiva.1	. . 3 ⊢ ((φ ∧ x ∈ A) → ψ)
2	1	ex 423	. 2 ⊢ (φ → (x ∈ A → ψ))
3	2	ralrimiv 2697	1 ⊢ (φ → ∀x ∈ A ψ)

Syntax hints:   → wi 4   ∧ wa 358   ∈ wcel 1710  ∀wral 2615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2620

This theorem is referenced by:  ralrimivvva  2708  rgen2  2711  rgen3  2712  nrexdv  2718  rabbidva  2851  ssrabdv  3346  ss2rabdv  3348  rgenz  3656  iuneq2dv  3991  ssofss  4077  findsd  4411  evenodddisj  4517  tfinnn  4535  vfinspss  4552  vfinspclt  4553  fun11iun  5306  eqfnfvd  5396  dff3  5421  dffo4  5424  foco2  5427  ffnfv  5428  ffvresb  5432  fconst2g  5453  fconstfv  5457  fmptd  5695  f1od  5727  extd  5924  refrd  5927  enmap2lem5  6068  enmap1lem5  6074  spacis  6289  nchoicelem12  6301  nchoicelem17  6306