![]() |
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 466 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
3 | 2 | ralbidva 3165 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | ralbidva 3165 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∈ wcel 2098 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ral 3051 |
This theorem is referenced by: disjxun 5147 reu3op 6298 opreu2reurex 6300 isocnv3 7339 isotr 7343 f1oweALT 7977 fnmpoovd 8092 pospropd 18322 tosso 18414 isipodrs 18532 mgmpropd 18614 mgmhmpropd 18661 sgrppropd 18694 mndpropd 18722 mhmpropd 18752 efgred 19715 cmnpropd 19758 rngpropd 20126 ringpropd 20236 lmodprop2d 20819 lsspropd 20914 islmhm2 20935 lmhmpropd 20970 isdomn3 21265 islindf4 21789 assapropd 21822 scmatmats 22457 cpmatel2 22659 1elcpmat 22661 m2cpminvid2 22701 decpmataa0 22714 pmatcollpw2lem 22723 connsub 23369 hausdiag 23593 ist0-4 23677 ismet2 24283 txmetcnp 24500 txmetcn 24501 metuel2 24518 metucn 24524 isngp3 24551 nlmvscn 24648 isclmp 25068 isncvsngp 25121 ipcn 25218 iscfil2 25238 caucfil 25255 cfilresi 25267 ulmdvlem3 26383 cxpcn3 26728 tgjustf 28349 tgjustr 28350 tgcgr4 28407 perpcom 28589 brbtwn2 28788 colinearalglem2 28790 eengtrkg 28869 isarchi2 32985 opprlidlabs 33297 elmrsubrn 35261 isbnd3b 37389 iscvlat2N 38926 ishlat3N 38956 gicabl 42665 lindslinindsimp2 47717 joindm3 48174 meetdm3 48176 functhinclem1 48233 postc 48274 |
Copyright terms: Public domain | W3C validator |