![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rabeqbidv | GIF version |
Description: Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.) |
Ref | Expression |
---|---|
rabeqbidv.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
rabeqbidv.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
rabeqbidv | ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabeqbidv.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | rabeq 2729 | . . 3 ⊢ (𝐴 = 𝐵 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) | |
3 | 1, 2 | syl 14 | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓}) |
4 | rabeqbidv.2 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
5 | 4 | rabbidv 2726 | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
6 | 3, 5 | eqtrd 2210 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 = wceq 1353 {crab 2459 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-rab 2464 |
This theorem is referenced by: elfvmptrab1 5610 mpoxopoveq 6240 supeq123d 6989 phival 12207 dfphi2 12214 ismhm 12807 issubm 12817 issubg 12986 subgex 12989 isnsg 13015 issubrg 13302 cldval 13492 neifval 13533 cnfval 13587 cnpfval 13588 cnprcl2k 13599 hmeofvalg 13696 ispsmet 13716 ismet 13737 isxmet 13738 blfvalps 13778 cncfval 13952 |
Copyright terms: Public domain | W3C validator |