Theorem r2al 3200

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 1972	. 2 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐵 → 𝜑)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐵 → 𝜑)))
2	1	r2allem 3152	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3079

This theorem is used by:  r2ex  3201  r3al  3202  ralcom  3292  nfra2w  3300  moel  3387  raliunxp  5823  codir  6118  qfto  6119  dfpo2  6298  fununi  6612  dff13  7255  mpo2eqb  7549  frpoins3xpg  8142  xpord2indlem  8149  tz7.48lem  8434  qliftfun  8806  zorn2lem4  10505  isirred2  20568  isdomn3  20882  cnmpt12  23899  cnmpt22  23906  dchrelbas3  27482  ons2ind  28548  cvmlift2lem12  35901  dfso2  36342  r2alan  39007  inxpss  39073  inxpss3  39076  dfac5prim  45821  permac8prim  45845  iscnrm3lem2  49869  joindm2  49902  meetdm2  49904