Theorem r2al 3198

Description: Double restricted universal quantification. (Contributed by NM, 19-Nov-1995.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Jan-2020.)

Assertion

Ref	Expression
r2al	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝐴(𝑥)   𝐵(𝑥, 𝑦)

Proof of Theorem r2al

Step	Hyp	Ref	Expression
1		19.21v 1971	. 2 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑)))
2	1	r2allem 3150	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3077

This theorem is used by:  r2ex  3199  r3al  3200  ralcom  3290  nfra2w  3298  moel  3385  raliunxp  5815  codir  6113  qfto  6114  dfpo2  6299  fununi  6615  dff13  7258  mpo2eqb  7552  frpoins3xpg  8157  xpord2indlem  8164  tz7.48lemOLD  8451  qliftfun  8823  zorn2lem4  10577  isirred2  20651  isdomn3  20966  cnmpt12  23986  cnmpt22  23993  dchrelbas3  27565  ons2ind  28661  cvmlift2lem12  36079  dfso2  36520  r2alan  39184  inxpss  39250  inxpss3  39253  dfac5prim  45980  permac8prim  46004  iscnrm3lem2  50043  joindm2  50076  meetdm2  50078