![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opabbii | Structured version Visualization version GIF version |
Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
Ref | Expression |
---|---|
opabbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
opabbii | ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2725 | . 2 ⊢ 𝑧 = 𝑧 | |
2 | opabbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | a1i 11 | . . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓)) |
4 | 3 | opabbidv 5215 | . 2 ⊢ (𝑧 = 𝑧 → {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓}) |
5 | 1, 4 | ax-mp 5 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1533 {copab 5211 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-opab 5212 |
This theorem is referenced by: mptv 5265 2rbropap 5568 dfid4 5577 fconstmpt 5740 xpundi 5746 xpundir 5747 inxpOLD 5835 csbcnv 5886 cnvco 5888 resopab 6039 opabresid 6054 cnvi 6148 cnvun 6149 cnvxp 6163 cnvcnv3 6194 coundi 6253 coundir 6254 mptun 6702 fvopab6 7038 fmptsng 7177 fmptsnd 7178 cbvoprab1 7507 cbvoprab12 7509 dmoprabss 7523 mpomptx 7533 resoprab 7538 elrnmpores 7559 ov6g 7585 1st2val 8022 2nd2val 8023 dfoprab3s 8058 dfoprab3 8059 dfoprab4 8060 opabn1stprc 8063 mptmpoopabbrd 8085 mptmpoopabbrdOLD 8086 mptmpoopabbrdOLDOLD 8088 fsplit 8122 mapsncnv 8912 xpcomco 9090 marypha2lem2 9466 oemapso 9712 ttrclresv 9747 leweon 10041 r0weon 10042 compsscnv 10401 fpwwe 10676 ltrelxr 11312 ltxrlt 11321 ltxr 13135 shftidt2 15069 prdsle 17452 prdsless 17453 prdsleval 17467 dfiso2 17763 joindm 18375 meetdm 18389 gaorb 19275 efgcpbllema 19726 frgpuplem 19744 dvdsrzring 21409 pjfval2 21665 ltbval 22008 ltbwe 22009 opsrle 22012 opsrtoslem1 22026 opsrtoslem2 22027 lmfval 23185 lmbr 23211 lgsquadlem3 27365 perpln1 28591 outpasch 28636 ishpg 28640 axcontlem2 28853 wksfval 29500 wlkson 29547 pthsfval 29612 ispth 29614 dfadj2 31772 dmadjss 31774 cnvadj 31779 mpomptxf 32550 lsmsnorb2 33209 satfv0 35101 satfvsuclem1 35102 satfvsuclem2 35103 satfbrsuc 35109 satf0 35115 satf0suclem 35118 fmlasuc0 35127 fneer 35970 bj-dfmpoa 36730 bj-mpomptALT 36731 bj-brab2a1 36761 bj-imdiridlem 36797 bj-opabco 36800 opropabco 37330 cnvepres 37902 inxp2 37971 disjecxrn 37993 xrninxp 37996 xrninxp2 37997 rnxrnres 38003 rnxrncnvepres 38004 rnxrnidres 38005 dfcoss2 38017 dfcoss3 38018 cosscnv 38020 coss1cnvres 38021 coss2cnvepres 38022 1cossres 38033 dfcoels 38034 ressn2 38046 br1cosscnvxrn 38078 1cosscnvxrn 38079 coss0 38083 cossid 38084 dfssr2 38103 cmtfvalN 38814 cmtvalN 38815 cvrfval 38872 cvrval 38873 dicval2 40784 aks6d1c1p1rcl 41713 aks6d1c1rh 41730 fgraphopab 42775 fgraphxp 42776 mptssid 44756 dfnelbr2 46793 opabbrfex0d 46806 opabbrfexd 46808 upwlksfval 47385 xpsnopab 47407 mpomptx2 47586 |
Copyright terms: Public domain | W3C validator |