![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > r19.26-2 | Structured version Visualization version GIF version |
Description: Restricted quantifier version of 19.26-2 1866. Version of r19.26 3105 with two quantifiers. (Contributed by NM, 10-Aug-2004.) |
Ref | Expression |
---|---|
r19.26-2 | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.26 3105 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) | |
2 | 1 | ralbii 3087 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) |
3 | r19.26 3105 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | |
4 | 2, 3 | bitri 275 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 ∀wral 3055 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ral 3056 |
This theorem is referenced by: fununi 6617 tz7.48lem 8442 isffth2 17878 ispos2 18280 issgrpv 18654 issgrpn0 18655 isnsg2 19083 efgred 19668 isrnghm 20343 dfrhm2 20376 df2idl2rng 21113 cpmatacl 22573 cpmatmcllem 22575 caucfil 25166 aalioulem6 26227 ajmoi 30620 adjmo 31594 prmidl2 33065 iccllysconn 34769 dfso3 35223 fvineqsnf1 36798 ispridl2 37419 ishlat2 38736 fiinfi 42900 ntrk1k3eqk13 43377 |
Copyright terms: Public domain | W3C validator |