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 468 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
3 | 2 | ralbidva 3196 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | ralbidva 3196 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜓 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∈ wcel 2105 ∀wral 3138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ral 3143 |
This theorem is referenced by: disjxun 5056 reu3op 6137 opreu2reurex 6139 isocnv3 7074 isotr 7078 f1oweALT 7664 fnmpoovd 7773 tosso 17636 pospropd 17734 isipodrs 17761 mndpropd 17926 mhmpropd 17952 efgred 18805 cmnpropd 18847 ringpropd 19263 lmodprop2d 19627 lsspropd 19720 islmhm2 19741 lmhmpropd 19776 assapropd 20031 islindf4 20912 scmatmats 21050 cpmatel2 21251 1elcpmat 21253 m2cpminvid2 21293 decpmataa0 21306 pmatcollpw2lem 21315 connsub 21959 hausdiag 22183 ist0-4 22267 ismet2 22872 txmetcnp 23086 txmetcn 23087 metuel2 23104 metucn 23110 isngp3 23136 nlmvscn 23225 isclmp 23630 isncvsngp 23682 ipcn 23778 iscfil2 23798 caucfil 23815 cfilresi 23827 ulmdvlem3 24919 cxpcn3 25256 tgjustf 26187 tgjustr 26188 tgcgr4 26245 perpcom 26427 brbtwn2 26619 colinearalglem2 26621 eengtrkg 26700 isarchi2 30742 elmrsubrn 32665 isbnd3b 34946 iscvlat2N 36342 ishlat3N 36372 gicabl 39579 isdomn3 39684 mgmpropd 43889 mgmhmpropd 43899 lidlmmgm 44094 lindslinindsimp2 44416 |
Copyright terms: Public domain | W3C validator |