Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ralimi2 | Structured version Visualization version GIF version |
Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 22-Feb-2004.) |
Ref | Expression |
---|---|
ralimi2.1 | ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓)) |
Ref | Expression |
---|---|
ralimi2 | ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralimi2.1 | . . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) → (𝑥 ∈ 𝐵 → 𝜓)) | |
2 | 1 | alimi 1806 | . 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝜑) → ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) |
3 | df-ral 3141 | . 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) | |
4 | df-ral 3141 | . 2 ⊢ (∀𝑥 ∈ 𝐵 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝜓)) | |
5 | 2, 3, 4 | 3imtr4i 294 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → ∀𝑥 ∈ 𝐵 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1529 ∈ wcel 2108 ∀wral 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 209 df-ral 3141 |
This theorem is referenced by: ralimia 3156 ralcom3 3363 tfi 7560 resixpfo 8492 omex 9098 kmlem1 9568 brdom5 9943 brdom4 9944 xrub 12697 pcmptcl 16219 itgeq2 24370 iblcnlem 24381 pntrsumbnd 26134 nmounbseqi 28546 nmounbseqiALT 28547 sumdmdi 30189 dmdbr4ati 30190 dmdbr6ati 30192 bnj110 32123 fiinfi 39923 |
Copyright terms: Public domain | W3C validator |