![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabbidva2 | Structured version Visualization version GIF version |
Description: Equivalent wff's yield equal restricted class abstractions. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
Ref | Expression |
---|---|
rabbidva2.1 | ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) |
Ref | Expression |
---|---|
rabbidva2 | ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabbidva2.1 | . . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐵 ∧ 𝜒))) | |
2 | 1 | abbidv 2802 | . 2 ⊢ (𝜑 → {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜒)}) |
3 | df-rab 3434 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} | |
4 | df-rab 3434 | . 2 ⊢ {𝑥 ∈ 𝐵 ∣ 𝜒} = {𝑥 ∣ (𝑥 ∈ 𝐵 ∧ 𝜒)} | |
5 | 2, 3, 4 | 3eqtr4g 2798 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 {cab 2710 {crab 3433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-rab 3434 |
This theorem is referenced by: rabbia2 3436 rabbidva 3440 rabeq 3447 extmptsuppeq 8173 dfac2a 10124 hashbclem 14411 umgrislfupgrlem 28382 wwlksn0s 29115 wwlksnextwrd 29151 wpthswwlks2on 29215 rusgrnumwwlkl1 29222 clwwlknon1 29350 orvcgteel 33466 orvclteel 33471 mapdvalc 40500 mapdval4N 40503 ovncvrrp 45280 ovnsubaddlem1 45286 ovnsubadd 45288 ovncvr2 45327 hspmbl 45345 smflim 45493 smflimsuplem1 45536 smflimsuplem3 45538 smflimsuplem7 45542 smflimsup 45544 |
Copyright terms: Public domain | W3C validator |