![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2ralbidva | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted universal quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 9-Dec-2019.) |
Ref | Expression |
---|---|
2ralbidva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2ralbidva | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2ralbidva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) | |
2 | 1 | anassrs 469 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
3 | 2 | ralbidva 3169 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | ralbidva 3169 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∈ wcel 2107 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ral 3062 |
This theorem is referenced by: disjxun 5104 reu3op 6245 opreu2reurex 6247 isocnv3 7278 isotr 7282 f1oweALT 7906 fnmpoovd 8020 pospropd 18221 tosso 18313 isipodrs 18431 mndpropd 18586 mhmpropd 18613 efgred 19535 cmnpropd 19578 ringpropd 20011 lmodprop2d 20399 lsspropd 20493 islmhm2 20514 lmhmpropd 20549 islindf4 21260 assapropd 21291 scmatmats 21876 cpmatel2 22078 1elcpmat 22080 m2cpminvid2 22120 decpmataa0 22133 pmatcollpw2lem 22142 connsub 22788 hausdiag 23012 ist0-4 23096 ismet2 23702 txmetcnp 23919 txmetcn 23920 metuel2 23937 metucn 23943 isngp3 23970 nlmvscn 24067 isclmp 24476 isncvsngp 24529 ipcn 24626 iscfil2 24646 caucfil 24663 cfilresi 24675 ulmdvlem3 25777 cxpcn3 26117 tgjustf 27457 tgjustr 27458 tgcgr4 27515 perpcom 27697 brbtwn2 27896 colinearalglem2 27898 eengtrkg 27977 isarchi2 32070 elmrsubrn 34171 isbnd3b 36290 iscvlat2N 37832 ishlat3N 37862 gicabl 41469 isdomn3 41574 mgmpropd 46155 mgmhmpropd 46165 lidlmmgm 46309 lindslinindsimp2 46630 joindm3 47088 meetdm3 47090 functhinclem1 47147 postc 47188 |
Copyright terms: Public domain | W3C validator |