| 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 467 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
| 3 | 2 | ralbidva 3176 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
| 4 | 3 | ralbidva 3176 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ral 3062 |
| This theorem is referenced by: disjxun 5141 reu3op 6312 opreu2reurex 6314 isocnv3 7352 isotr 7356 f1oweALT 7997 fnmpoovd 8112 pospropd 18372 tosso 18464 isipodrs 18582 mgmpropd 18664 mgmhmpropd 18711 sgrppropd 18744 mndpropd 18772 mhmpropd 18805 efgred 19766 cmnpropd 19809 rngpropd 20171 ringpropd 20285 isdomn3 20715 lmodprop2d 20922 lsspropd 21016 islmhm2 21037 lmhmpropd 21072 islindf4 21858 assapropd 21892 scmatmats 22517 cpmatel2 22719 1elcpmat 22721 m2cpminvid2 22761 decpmataa0 22774 pmatcollpw2lem 22783 connsub 23429 hausdiag 23653 ist0-4 23737 ismet2 24343 txmetcnp 24560 txmetcn 24561 metuel2 24578 metucn 24584 isngp3 24611 nlmvscn 24708 isclmp 25130 isncvsngp 25183 ipcn 25280 iscfil2 25300 caucfil 25317 cfilresi 25329 ulmdvlem3 26445 cxpcn3 26791 tgjustf 28481 tgjustr 28482 tgcgr4 28539 perpcom 28721 brbtwn2 28920 colinearalglem2 28922 eengtrkg 29001 isarchi2 33192 opprlidlabs 33513 elmrsubrn 35525 isbnd3b 37792 iscvlat2N 39325 ishlat3N 39355 gicabl 43111 lindslinindsimp2 48380 joindm3 48866 meetdm3 48868 fucofulem2 49006 thincpropd 49091 functhinclem1 49093 fulltermc 49143 postc 49173 |
| Copyright terms: Public domain | W3C validator |