Theorem r19.26-2 3139

Description: Restricted quantifier version of 19.26-2 1875. Version of r19.26 3112 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 3112	. . 3 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓))
2	1	ralbii 3094	. 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓))
3		r19.26 3112	. 2 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))
4	2, 3	bitri 275	1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 205   ∧ wa 397  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3063

This theorem is referenced by:  fununi  6620  tz7.48lem  8436  isffth2  17863  ispos2  18264  issgrpv  18608  issgrpn0  18609  isnsg2  19030  efgred  19609  dfrhm2  20242  df2idl2  20847  cpmatacl  22200  cpmatmcllem  22202  caucfil  24782  aalioulem6  25832  ajmoi  30089  adjmo  31063  prmidl2  32517  iccllysconn  34179  dfso3  34627  fvineqsnf1  36229  ispridl2  36844  ishlat2  38161  fiinfi  42257  ntrk1k3eqk13  42734  isrnghm  46624