Theorem r19.21v 3159

Description: Restricted quantifier version of 19.21v 1940. (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 42	. . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	ralimdv 3148	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3130	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3071	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 186	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wral 3049

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3050

This theorem is referenced by:  r19.23v  3161  r19.32v  3167  cbvraldva  3214  rmo4  3686  2reu5lem3  3713  ra4v  3833  rmo3  3837  dftr5  5207  reusv3  5348  tfinds2  7804  tfinds3  7805  fpr3g  8225  wfr3g  8259  tfrlem1  8305  tfr3  8328  oeordi  8513  naddssim  8611  ordiso2  9418  ordtypelem7  9427  cantnf  9600  dfac12lem3  10054  ttukeylem5  10421  ttukeylem6  10422  fpwwe2lem7  10546  grudomon  10726  raluz2  12808  bpolycl  15973  ndvdssub  16334  gcdcllem1  16424  acsfn2  17584  pgpfac1  20009  pgpfac  20013  isdomn5  20641  isdomn2OLD  20643  islindf4  21791  isclo2  23030  1stccn  23405  kgencn  23498  txflf  23948  fclsopn  23956  conway  27767  nn0min  32850  bnj580  35018  bnj852  35026  rdgprc  35935  filnetlem4  36524  poimirlem29  37789  heicant  37795  indstrd  42386  ntrneixb  44278  trfr  45145  modelac8prim  45175  2rexrsb  47290  tfis2d  49867