![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralimdv2 | Structured version Visualization version GIF version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 1-Feb-2005.) |
Ref | Expression |
---|---|
ralimdv2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) |
Ref | Expression |
---|---|
ralimdv2 | ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimdv2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 → 𝜓) → (𝑥 ∈ 𝐵 → 𝜒))) | |
2 | 1 | alimdv 1912 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) |
3 | df-ral 3052 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
4 | df-ral 3052 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
5 | 2, 3, 4 | 3imtr4g 295 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1532 ∈ wcel 2099 ∀wral 3051 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 |
This theorem depends on definitions: df-bi 206 df-ral 3052 |
This theorem is referenced by: ralimdva 3157 ssralvOLD 4052 zorn2lem7 10545 pwfseqlem3 10703 sup2 12222 xrsupexmnf 13338 xrinfmexpnf 13339 xrsupsslem 13340 xrinfmsslem 13341 xrub 13345 r19.29uz 15355 rexuzre 15357 caurcvg 15681 caucvg 15683 isprm5 16708 prmgaplem5 17057 prmgaplem6 17058 mrissmrid 17654 elcls3 23078 iscnp4 23258 cncls2 23268 cnntr 23270 2ndcsep 23454 dyadmbllem 25619 xrlimcnp 26996 pntlem3 27638 sigaclfu2 33954 lfuhgr2 34946 rdgssun 37085 mapdordlem2 41336 aks6d1c1 41814 sn-sup2 42251 dffltz 42288 cantnfresb 42990 safesnsupfiub 43083 iunrelexp0 43369 climrec 45224 0ellimcdiv 45270 pgindnf 48462 |
Copyright terms: Public domain | W3C validator |