Theorem r19.26-2 3118

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

Syntax hints:   ↔ wb 206   ∧ wa 395  ∀wral 3044

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 207  df-an 396  df-ral 3045

This theorem is referenced by:  fununi  6591  tz7.48lem  8409  isffth2  17880  ispos2  18276  issgrpv  18648  issgrpn0  18649  isnsg2  19088  efgred  19678  isrnghm  20350  dfrhm2  20383  df2idl2rng  21166  cpmatacl  22603  cpmatmcllem  22605  caucfil  25183  aalioulem6  26245  ajmoi  30787  adjmo  31761  prmidl2  33412  iccllysconn  35237  dfso3  35707  fvineqsnf1  37398  ispridl2  38032  ishlat2  39346  fiinfi  43562  ntrk1k3eqk13  44039