![]() |
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 1874. Version of r19.26 3111 with two quantifiers. (Contributed by NM, 10-Aug-2004.) |
Ref | Expression |
---|---|
r19.26-2 | ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | r19.26 3111 | . . 3 ⊢ (∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) | |
2 | 1 | ralbii 3093 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓)) |
3 | r19.26 3111 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑦 ∈ 𝐵 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) | |
4 | 2, 3 | bitri 274 | 1 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ral 3062 |
This theorem is referenced by: fununi 6623 tz7.48lem 8440 isffth2 17866 ispos2 18267 issgrpv 18611 issgrpn0 18612 isnsg2 19035 efgred 19615 dfrhm2 20252 df2idl2 20859 cpmatacl 22217 cpmatmcllem 22219 caucfil 24799 aalioulem6 25849 ajmoi 30106 adjmo 31080 prmidl2 32554 iccllysconn 34236 dfso3 34684 fvineqsnf1 36286 ispridl2 36901 ishlat2 38218 fiinfi 42314 ntrk1k3eqk13 42791 isrnghm 46680 df2idl2rng 46749 |
Copyright terms: Public domain | W3C validator |