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 1908 | . 2 ⊢ (𝜑 → (∀𝑥(𝑥 ∈ 𝐴 → 𝜓) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜒))) |
3 | df-ral 3140 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)) | |
4 | df-ral 3140 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜒 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜒)) | |
5 | 2, 3, 4 | 3imtr4g 297 | 1 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐵 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1526 ∈ wcel 2105 ∀wral 3135 |
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-ral 3140 |
This theorem is referenced by: ralimdva 3174 ssralv 4030 zorn2lem7 9912 pwfseqlem3 10070 sup2 11585 xrsupexmnf 12686 xrinfmexpnf 12687 xrsupsslem 12688 xrinfmsslem 12689 xrub 12693 r19.29uz 14698 rexuzre 14700 caurcvg 15021 caucvg 15023 isprm5 16039 prmgaplem5 16379 prmgaplem6 16380 mrissmrid 16900 elcls3 21619 iscnp4 21799 cncls2 21809 cnntr 21811 2ndcsep 21995 dyadmbllem 24127 xrlimcnp 25473 pntlem3 26112 sigaclfu2 31279 lfuhgr2 32262 rdgssun 34541 mapdordlem2 38653 dffltz 39149 iunrelexp0 39925 climrec 41760 0ellimcdiv 41806 |
Copyright terms: Public domain | W3C validator |