![]() |
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 460 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
3 | 2 | ralbidva 3146 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | ralbidva 3146 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∈ wcel 2050 ∀wral 3088 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ral 3093 |
This theorem is referenced by: disjxun 4927 reu3op 5981 opreu2reurex 5983 isocnv3 6908 isotr 6912 f1oweALT 7485 fnmpoovd 7590 tosso 17504 pospropd 17602 isipodrs 17629 mndpropd 17784 mhmpropd 17809 efgred 18634 cmnpropd 18675 ringpropd 19055 lmodprop2d 19418 lsspropd 19511 islmhm2 19532 lmhmpropd 19567 assapropd 19821 islindf4 20684 scmatmats 20824 cpmatel2 21025 1elcpmat 21027 m2cpminvid2 21067 decpmataa0 21080 pmatcollpw2lem 21089 connsub 21733 hausdiag 21957 ist0-4 22041 ismet2 22646 txmetcnp 22860 txmetcn 22861 metuel2 22878 metucn 22884 isngp3 22910 nlmvscn 22999 isclmp 23404 isncvsngp 23456 ipcn 23552 iscfil2 23572 caucfil 23589 cfilresi 23601 ulmdvlem3 24693 cxpcn3 25030 tgjustf 25961 tgjustr 25962 tgcgr4 26019 perpcom 26201 brbtwn2 26394 colinearalglem2 26396 eengtrkg 26475 isarchi2 30486 elmrsubrn 32293 isbnd3b 34511 iscvlat2N 35911 ishlat3N 35941 gicabl 39101 isdomn3 39206 mgmpropd 43416 mgmhmpropd 43426 lidlmmgm 43566 lindslinindsimp2 43891 |
Copyright terms: Public domain | W3C validator |