Theorem r19.21v 3196

Description: Restricted quantifier version of 19.21v 1966. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 11-Dec-2024.)

Assertion

Ref	Expression
r19.21v	⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem r19.21v

Step	Hyp	Ref	Expression
1		pm2.27 43	. . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	ralimdv 3185	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 33	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 124	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3167	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3108	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 188	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086

This theorem is referenced by:  r19.23v  3198  r19.32v  3204  cbvraldva  3251  rmo4  3702  2reu5lem3  3729  ra4v  3847  rmo3  3851  dftr5  5226  reusv3  5377  tfinds2  7859  tfinds3  7860  fpr3g  8281  wfr3g  8315  tfrlem1  8361  tfr3  8385  oeordi  8572  naddssim  8671  ordiso2  9476  ordtypelem7  9485  cantnf  9661  dfac12lem3  10128  ttukeylem5  10496  ttukeylem6  10497  fpwwe2lem7  10621  grudomon  10801  raluz2  12920  bpolycl  16105  ndvdssub  16466  gcdcllem1  16556  acsfn2  17718  pgpfac1  20151  pgpfac  20155  isdomn5  20794  islindf4  21956  isclo2  23213  1stccn  23588  kgencn  23681  txflf  24131  fclsopn  24139  conway  27937  nn0min  33105  bnj580  35245  bnj852  35253  rdgprc  36182  filnetlem4  36780  poimirlem29  38187  heicant  38193  indstrd  42849  ntrneixb  44712  trfr  45562  modelac8prim  45592  2rexrsb  47727  tfis2d  50342