Theorem r19.26-2 3136

Description: Restricted quantifier version of 19.26-2 1872. Version of r19.26 3109 with two quantifiers. (Contributed by NM, 10-Aug-2004.)

Assertion

Ref	Expression
r19.26-2	⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))

Proof of Theorem r19.26-2

Step	Hyp	Ref	Expression
1		r19.26 3109	. . 3 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓))
2	1	ralbii 3091	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓))
3		r19.26 3109	. 2 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))
4	2, 3	bitri 274	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 394  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 206  df-an 395  df-ral 3060

This theorem is referenced by:  fununi  6622  tz7.48lem  8443  isffth2  17871  ispos2  18272  issgrpv  18646  issgrpn0  18647  isnsg2  19072  efgred  19657  isrnghm  20332  dfrhm2  20365  df2idl2  21009  df2idl2rng  21037  cpmatacl  22438  cpmatmcllem  22440  caucfil  25031  aalioulem6  26086  ajmoi  30378  adjmo  31352  prmidl2  32833  iccllysconn  34539  dfso3  34993  fvineqsnf1  36594  ispridl2  37209  ishlat2  38526  fiinfi  42626  ntrk1k3eqk13  43103