New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > raleqbi1dv | GIF version |
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) |
Ref | Expression |
---|---|
raleqd.1 | ⊢ (A = B → (φ ↔ ψ)) |
Ref | Expression |
---|---|
raleqbi1dv | ⊢ (A = B → (∀x ∈ A φ ↔ ∀x ∈ B ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq 2807 | . 2 ⊢ (A = B → (∀x ∈ A φ ↔ ∀x ∈ B φ)) | |
2 | raleqd.1 | . . 3 ⊢ (A = B → (φ ↔ ψ)) | |
3 | 2 | ralbidv 2634 | . 2 ⊢ (A = B → (∀x ∈ B φ ↔ ∀x ∈ B ψ)) |
4 | 1, 3 | bitrd 244 | 1 ⊢ (A = B → (∀x ∈ A φ ↔ ∀x ∈ B ψ)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 176 = wceq 1642 ∀wral 2614 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ral 2619 |
This theorem is referenced by: peano5 4409 ncfinraise 4481 nnadjoin 4520 nnpweq 4523 tfinnn 4534 spfininduct 4540 isoeq4 5485 trd 5921 extd 5923 symd 5924 trrd 5925 antird 5928 antid 5929 connexrd 5930 connexd 5931 iserd 5942 |
Copyright terms: Public domain | W3C validator |