Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ralbiia | GIF version |
Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.) |
Ref | Expression |
---|---|
ralbiia.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
ralbiia | ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralbiia.1 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) | |
2 | 1 | pm5.74i 179 | . 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓)) |
3 | 2 | ralbii2 2474 | 1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∈ wcel 2135 ∀wral 2442 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 |
This theorem depends on definitions: df-bi 116 df-ral 2447 |
This theorem is referenced by: frind 4324 poinxp 4667 soinxp 4668 seinxp 4669 dffun8 5210 funcnv3 5244 fncnv 5248 fnres 5298 fvreseq 5583 isoini2 5781 smores 6251 resixp 6690 pw1dc1 6870 finomni 7095 caucvgre 10909 bj-charfundcALT 13526 |
Copyright terms: Public domain | W3C validator |